Require Import Coq.omega.Omega.

Lemma strong_induction {P: nat -> Prop}:
  (forall n, (forall m, m < n -> P m) -> P n) ->
  (forall n, P n).
Proof.
(* Goal: forall (_ : forall (n : nat) (_ : forall (m : nat) (_ : lt m n), P m), P n) (n : nat), P n *)
  intros ?.
(* Goal: forall n : nat, P n *)
  assert (forall n, (forall m, m < n -> P m)).
  + intro n; induction n.
    - intros; omega.
    - intros.
(* Goal: P m *)
      destruct (lt_dec m n).
      * apply IHn; auto.
      * assert (m = n) by omega; subst m.
(* Goal: P n *)
        apply H; auto.
  + intros.
(* Goal: P n *)
    apply (H0 (S n)).
(* Goal: lt n (S n) *)
    constructor.
Qed.

Ltac strong_induction n :=
  revert dependent n;
  intro n;
  pattern n;
  revert n;
  apply strong_induction;
  intros ?n ?IH.
