a b : binint_pred_double (binint_pos_sub (pos_succ a) b) = binint_succ_double (binint_pos_sub a b). Proof. revert a b. induction a; induction b; trivial. + by destruct b. + by destruct b. + cbn; by destruct (binint_pos_sub a b). + cbn; by destruct (binint_pos_sub a b). + cbn; apply ap. by rewrite pos_pred_double_succ. + cbn. rewrite <- IHa. by destruct (binint_pos_sub (pos_succ a) b). + cbn. rewrite IHa. by destruct (binint_pos_sub a b). Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.