Strong induction for nat in Coq

Question

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.

Answer 1

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.