proposition: Lemma lt_wf : well_founded lt.
proof: Proof. intro n; induction n. - split; intro p; inversion 1. - split; intros y Hy; assert (H: y < n \/ y = n) by lia. destruct H. + now apply IHn. + now subst. Qed.
imports: Coq(FunInd Recdef Wf_nat Lia)