binint_succ o binint_pred == idmap. Proof. intros [n | | n]; [|trivial|]. all: destruct n; trivial. 1,2: cbn; apply ap. 1: apply pos_pred_double_succ. rewrite pos_add_1_r. apply pos_succ_pred_double. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.