proposition: Lemma mul_omega2_pr1 a (u:= cons one 1 zero): a != zero -> T1nf a -> sup (T1mul a) u (a * u).
proof: Proof. move => sa sb. have sc: T1nf u by []. split. by apply: nf_mul. by move => y ny /T1ltW; rewrite (T1le_mul2l _ sa ny). move => z nz zp. have eq1: a * u = a* T1omega + a * T1omega by rewrite - mul_distr //. case: (T1ltP z (a* T1omega)) => zo; first by exists T1omega => //. move: (sub_pr1 nz zo) => sd. move: (mul_omega_pr1 sa sb) => [se _ sf]. move: zp; rewrite sd eq1; rewrite T1lt_add2l => sg. move: (sf _ (nf_sub nz se) sg) => [y1 /and3P [ya yb yc]]. exists (T1omega + y1); by rewrite nf_add // -[u] /(T1omega +T1omega) mul_distr !T1lt_add2l yb yc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)