proposition: Theorem pair_induction : A 0 -> A 1 -> (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.
proof: Proof. rewrite one_succ. intros until 3. assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. intro n; induct n; [ | intros n [IH1 IH2]]; auto. Qed.
imports: Decidable NAxioms NZProperties