proposition: Lemma omega_least_inf2 x: ~~ T2finite x -> omega <= x.
proof: Proof. case: x => // a b n c. rewrite /omega T2le_consE /= /lt_psi !T2lt0n !T2ltn0 /= !T2gt1 => eq1. rewrite eq1; move:eq1; rewrite T2eqE !orbF /= !andbT (eq_sym a zero). case pa: (zero==a) => //= -> /=; rewrite (eq_sym b); case: (one==b) => //. by rewrite T2le0n; case: n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)