a b : binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b. Proof. rewrite <- 2 pos_add_1_r. revert a b. induction a; induction b; trivial. 1: destruct b; trivial. { destruct b; trivial. cbn; apply ap. by rewrite pos_pred_double_succ. } 1: destruct a; trivial. 1: apply binint_succ_double_binint_pos_sub. { destruct a; trivial. cbn; apply ap, ap, pos_pred_double_succ. } 1: apply binint_pred_double_binint_pos_sub. cbn; apply ap. rewrite <- 2 pos_add_1_r. apply IHa. Defined.
Require Import Basics. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core.