proposition: Proposition strong_induction (P : nat -> Type) : (forall n : nat, (forall m : nat, (m < n) -> P m) -> P n) -> forall n : nat, P n.
proof: Proof. intro a. assert (forall n m: nat, m < n -> P m) as X. { simple_induction n n IHn. - intros m l. contradiction (not_lt_n_0 m). - intros m l. apply leq_S_n in l. destruct l as [ | n]. + apply a; intros ? ?; now apply IHn. + now apply (IHn m), leq_S_n'. } intro n. apply (X (n.+1) n), (leq_n n.+1). Defined.
imports: Basics Spaces.Nat.Core