proposition: Lemma mul_omega_pr1 a: a != zero -> T1nf a -> sup (T1mul a) T1omega (a * T1omega).
proof: Proof. move => sa sb. have sc: T1nf T1omega by []. split; first by apply: nf_mul. by move => y ny /T1ltW; rewrite (T1le_mul2l _ sa ny). move => z nz zp. move: sb sa zp; case: a => // a1 n1 b1 sb _; rewrite /= andbF. move: nz; case z; first by exists one => //=; case: (_ && _). move => a2 n2 b2 /= /and3P [ha hb hc]. rewrite T1ltn0 !if_same if_simpl - succ_is_add_one lt_succ_le_3 //. case /orP => a12; last first. exists one; simpl; move: a12; case az:(a1==zero); last by move => /= ->. by rewrite (eqP az) T1ltn0. rewrite (eqP a12). exists (\F (n2.+2)); case az: (a1==zero). by rewrite /= az /= T1ltn0 az addnS ltnS leq_addl. by rewrite /= az /= T1ltnn eqxx addnS ltnS leq_addl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)