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