proposition: Theorem bi_induction : A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
proof: Proof. Open Scope NScope. intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *. destruct n as [n m]. cut (forall p, A (p, 0)); [intro H1 |]. - cut (forall p, A (0, p)); [intro H2 |]. + destruct (add_dichotomy n m) as [[p H] | [p H]]. * rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. * rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. + induct p. * assumption. * intros p IH. apply (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. rewrite one_succ in IH. now apply AS. - induct p. + assumption. + intros p IH. replace 0 with (snd (p, 0)); [| reflexivity]. replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS. Close Scope NScope. Qed.
imports: NSub ZAxioms Ring