proposition: Lemma int_pred_pos_sub_r a b : int_pred (int_pos_sub a b) = int_pos_sub a (pos_succ b).
proof: 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 int_pos_sub_succ_succ. apply bH. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core