proposition: Lemma wf_ltn: well_founded (fun n => [eta ltn n]).
proof: Proof. move => n; apply Acc_incl with lt. - by move => i j /ltP. - apply lt_wf. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)