proposition: Lemma int_pred_add_r a b : int_pred (a + b) = a + int_pred b.
proof: 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 (int_pred_succ (neg a)). - intro a. rewrite <- pos_add_1_r. rewrite (int_pred_succ (pos b)). rewrite int_add_comm. cbn. rewrite pos_add_1_r. rewrite <- int_pos_sub_negation. rewrite <- int_pred_pos_sub_r. apply int_negation_inj. rewrite int_pos_sub_negation. apply int_negation_pred_negation_red. + cbn. rewrite pos_add_1_r. apply int_pred_pos_sub_r. + revert a. induction b as [|b bH] using pos_peano_ind. - intro a; exact (int_pred_succ (pos a)). - intro a. rewrite <- pos_add_1_r. rewrite (int_pred_succ (pos b)). cbn; rewrite pos_add_assoc. change (int_pred (int_succ (pos (a + b)%pos)) = pos a + pos b). apply int_pred_succ. Defined.
imports: Basics Spaces.Pos Spaces.Int.Core