proposition: Lemma finord_lt_wf n : well_founded (@finord_lt n).
proof: Proof. pose m (n:nat) (x:'I_n) := nat_of_ord x. move => x; rewrite /finord_lt. apply Acc_incl with (fun x y => m _ x < m _ y)%N. - move => a b; by rewrite /m. - apply (Acc_inverse_image ('I_n) nat (fun n p => (n < p)%N) (@m n) x), lt_wf. Qed.
imports: hydras(DecPreOrder ON_Generic) mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec)