Library Coqtail.Arith.Ninductions


Require Import Arith MyNat.

Lemma nat_strong : (P : natProp), P O
 ( N, ( n, (n N)%natP n) → P (S N)) → n, P n.
Proof.
intros P PO PS ; assert (H : N n, (n N)%natP n).
 intro N ; induction N ; intros n nleN ; inversion_clear nleN.
  assumption.
  apply PS, IHN.
  apply IHN ; assumption.
 intro n ; apply H with n ; reflexivity.
Qed.

Lemma nat_ind2 : (P : natProp),
  P OP (S O) → ( m, P mP (S (S m))) → n, P n.
Proof.
intros P P0 P1 PSS ; apply nat_strong.
 assumption.
 intros [] HN.
  assumption.
  apply PSS, HN, le_n_Sn.
Qed.