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