p q r : p + (q + r) = p + q + r. Proof. revert q r. induction p. + intros [|q|q] [|r|r]. all: try reflexivity. all: simpl. 1,2: by destruct r. 1,2: apply ap; symmetry. 1: apply pos_add_carry_spec. 1: apply pos_add_succ_l. apply ap. rewrite pos_add_succ_l. apply pos_add_carry_spec. + intros [|q|q] [|r|r]. all: try reflexivity. all: cbn; apply ap. 3,4,6: apply IHp. 1: apply pos_add_1_r. 1: symmetry; apply pos_add_carry_spec_r. 1: apply pos_add_succ_r. rewrite 2 pos_add_carry_spec_l. rewrite <- pos_add_succ_r. apply IHp. + intros [|q|q] [|r|r]. all: cbn; apply ap. 1: apply pos_add_1_r. 1: apply pos_add_carry_spec_l. 1: apply pos_add_succ. 1: apply pos_add_carry_spec. 1: apply IHp. 2: symmetry; apply pos_add_carry_spec_r. 1,2: rewrite 2 pos_add_carry_spec, ?pos_add_succ_l. 1,2: apply ap, IHp. rewrite ?pos_add_carry_spec_r. rewrite pos_add_succ. apply IHp. Qed.
Require Import Basics.Overture Basics.Tactics. Require Import Pos.Core.