x : - binint_pred (- binint_pred x) = x. Proof. destruct x as [x| |x]; trivial; destruct x; trivial; 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.