proposition: Lemma omega_least_inf1 x: T2finite x -> x < omega.
proof: Proof. case: x => // a b n c /= /eqP [] -> ->. by rewrite /omega T2lt_consE /lt_psi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)