proposition: Lemma lt_wf: well_founded (fun (a b:nat) => a < b).
proof: Proof. move => n; split;elim: n; first by move => y ; rewrite ltn0. move => n H y; rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->. by apply: H. Defined.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)