# Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat:

Lemma strong_ind (P : nat -> Prop) :
(forall m, (forall k : nat, k < m -> P k) -> P m) -> forall n, P n.


I've seen similar question on StackOverflow, but this doesn't really helped me. Currently, I have the following:

Proof.
intros. induction n. specialize (H 0) as H0. apply H0. intros. inversion H1.
specialize (H (S n)) as HSn. apply HSn. induction k.
- intros. apply H. intros. inversion H1.
- intros. apply Lt.lt_S_n in H0. apply PeanoNat.Nat.lt_lt_succ_r in H0. apply IHk in H0.


With the next context and goal:

1 goal
P : nat -> Prop
H : forall m : nat, (forall k : nat, k < m -> P k) -> P m
n : nat
IHn : P n
HSn : (forall k : nat, k < S n -> P k) -> P (S n)
k : nat
IHk : k < S n -> P k
H0 : P k
______________________________________(1/1)
P (S k)


I had similar goal before doing specialize (H (S n)) as HSn. already, since it was the induction step. So it feels like really I haven't gotten really any much progress. I've tried doing this in different ways, but still was stuck.

It feels like I should do twice induction as I did before (induction by n, then by k), but it seems I miss something which this "something" is crucial. I also don't see any other way to get things of form P (S _) except applying H every time, but it seems to me that this isn't the way it solves. I also think that I need somehow get forall k : nat, k < m -> P k into my context, I guess this (or something very similar to that) really solves my problem, but probably I don't know enough tactics to retrieve it.

Can anyone help me with this? Thanks in advance!

Edited: thanks to @Pierre Castéran, I have found the solution. But I'm 100% sure the solution can be optimized and shortened. My solution is the following:

Lemma strong_ind (P : nat -> Prop) :
(forall m, (forall k : nat, k < m -> P k) -> P m) ->
forall n, P n.
Proof.
intros H n; enough (H0: forall p, p <= n -> P p).
- apply H0, le_n.
- induction n.
+ intros. inversion H0. apply H. intros. inversion H2.
+ intros. apply H. intros. apply IHn.  inversion H0.
* rewrite H2 in H1. apply Lt.lt_n_Sm_le in H1. assumption.
* specialize (PeanoNat.Nat.lt_le_trans k p n H1 H3). apply PeanoNat.Nat.lt_le_incl.
Qed.

• In my experience, it's easier to prove (forall m, (forall k : nat, k < m -> P k) -> P m) -> (forall m k, k < m -> P k) where the outer k < m acts as some kind of accumulator. I have a proof like that with fancy types. Jun 13, 2022 at 18:10

A classic solution is to define a stronger property, which you prove by induction.

Lemma strong_ind (P : nat -> Prop) :
(forall m, (forall k : nat, k < m -> P k) -> P m) ->
forall n, P n.
Proof.
intros H n; enough (H0: forall p, p <= n -> P p).
- apply H0, le_n.
- induction n.
(* ... *)
Qed.

• Thank you! Via this, I've solved the puzzle. The only thing is that perhaps my solution is not optimal and maybe it might be shorten. Jun 13, 2022 at 17:00