proposition: Lemma lt_wf (n:nat) : well_founded (@lt n).
proof: Proof. intro x; apply Acc_incl with (fun alpha beta => proj1_sig alpha < proj1_sig beta)%nat. - intros [y Hy] [z Hz]; unfold lt; cbn; intro H. destruct z. + discriminate. + apply leb_complete in H; lia. - apply Acc_inverse_image, Wf_nat.lt_wf. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)