proposition: Lemma lte_wf: well_founded lte.
proof: Proof. suff: forall n, Acc lte n /\ Acc lte n.+1. by move => h n; move: (h n) => []. elim. by split; split => y; rewrite /lte /= ? ltn0 andbF. move => n [sa sb]; split; first by exact. split => y; rewrite /lte /=; move => /and3P[oy on]. rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->. rewrite ltnS leq_eqVlt; case /orP; first by move => /eqP ->. by move => yn; case sa; apply; rewrite /lte /= oy yn (negbNE on). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)