proposition: Lemma mul_omega_limit x: x != zero -> T1limit (T1omega * x).
proof: Proof. elim: x => // a _ n b Hb _. rewrite T1mul_omega; case pa: (a==zero) => //. rewrite /T1limit T1add_eq0 pa andbF -/T1limit. case pb: (b== zero). by rewrite (eqP pb) T1muln0. by rewrite (Hb (negbT pb)) orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)