proposition: Lemma omega_lt_wf : @well_founded Order.NatOrder.orderType <%O.
proof: Proof. exact: wf_ltn. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)