talia_2021_mar_11.v

Require Import Coq.NArith.NArith.

Theorem add_1_r : forall p, (p + 1)%positive = Pos.succ p.
Proof.
  induction p; simpl; eauto.
Qed.

Theorem add_carry_spec : forall p q, Pos.add_carry p q = Pos.succ (p + q).
Proof.
  induction p; induction q; simpl; eauto.
  all: f_equal; eauto.
Qed.  
  
Theorem talia : forall n m,
    N.succ (N.add n m) = N.add n (N.succ m).
Proof.
  induction n; induction m; simpl; try reflexivity.
  induction p; simpl; try reflexivity.  
  f_equal.
  generalize dependent p0.
  induction p; induction p0; simpl; try reflexivity.
  all: f_equal.
  all: rewrite ?add_carry_spec.
  all: try eapply IHp.
  all: eauto.
  all: rewrite add_1_r.
  all: eauto.
Qed.