proposition: Lemma omega_least_inf2 x: ~~ T3finite x -> omega <= x.
proof: Proof. case: x => // a b c n d. rewrite /T3finite /all_zero /T3le/omega T3lt_consE T3lt_psi /lt_psi. rewrite !T3lt0n !T3ltn0 /= (eq_sym a zero) (eq_sym b zero) !T3gt1 !andbF /=. rewrite (eq_sym [a,b,c] one) (eq_sym c one) (eq_sym d zero) !T3eqE. case: (zero == a) => //; case : (zero == b) => //= -> /=. by case h2: (one == c) => //; case: (ltngtP 0 n) => //=; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)