a b : binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b). Proof. revert a. induction b as [|b bH] using pos_peano_ind. 1: destruct a; trivial; destruct a; trivial. intro a. revert b bH. induction a as [|a aH] using pos_peano_ind. { intros b bH. rewrite <- bH. destruct b; trivial. cbn; apply ap. rewrite 2 pos_add_1_r. rewrite pos_succ_pred_double. rewrite pos_pred_double_succ. trivial. } intros b bH. rewrite 2 binint_pos_sub_succ_succ. apply bH. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.