proposition: Lemma nat_strong_ind : forall P : nat -> Prop, P 0 -> (forall n, (forall k, k<=n -> P k) -> P(S n)) -> forall n, P n.
proof: Proof. intros. assert (forall n, (forall k, k<=n -> P k)). apply (nat_ind (fun n=>forall k, k<=n -> P k)). intros. apply Nat.le_0_r in H1. rewrite H1. exact H. intros. apply le_le_S_eq in H2. destruct H2. apply H1. auto with arith. rewrite H2. apply H0. exact H1. apply H1 with n. auto with arith. Qed.
imports: PeanoNat Compare