proposition: Lemma lt_wf_ind : forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
proof: Proof. intro p; intros; elim (lt_wf p); auto with arith. Defined.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts)