a b : binint_pred (a + b) = a + binint_pred b. Proof. revert a b. intros [a| |a] [b| |b]; trivial. + cbn; apply ap. by rewrite pos_add_assoc. + revert a. induction b as [|b bH] using pos_peano_ind. - intro a; exact (binint_pred_succ (neg a)). - intro a. rewrite <- pos_add_1_r. rewrite (binint_pred_succ (pos b)). rewrite binint_add_comm. cbn. rewrite pos_add_1_r. rewrite <- binint_pos_sub_negation. rewrite <- binint_pred_pos_sub_r. apply binint_negation_inj. rewrite binint_pos_sub_negation. apply binint_negation_pred_negation_red. + cbn. rewrite pos_add_1_r. apply binint_pred_pos_sub_r. + revert a. induction b as [|b bH] using pos_peano_ind. - intro a; exact (binint_pred_succ (pos a)). - intro a. rewrite <- pos_add_1_r. rewrite (binint_pred_succ (pos b)). cbn; rewrite pos_add_assoc. change (binint_pred (binint_succ (pos (a + b)%pos)) = pos a + pos b). apply binint_pred_succ. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.