proposition: Lemma mul_omega_pr3 a b c: a != zero -> c != zero -> T1nf a -> T1nf b -> T1nf c -> sup (T1mul a) c (a * c) -> sup (T1mul a) (b+c) (a * (b + c)).
proof: Proof. move => az cz na nb nc [pa _ pc]; split => //. by apply: nf_mul => //; apply: nf_add. by move => y ny ybc; rewrite T1le_mul2l // T1ltW. move => z nz zle. case: (T1ltP z (a* b)) => zo. by exists b; rewrite nb zo add_le4. move: (sub_pr1 nz zo) => sd. move: zle; rewrite sd mul_distr T1lt_add2l => se. move: (pc _ (nf_sub nz (nf_mul na nb)) se) => [y1 /and3P [ya yb yc]]. by exists (b + y1); rewrite nf_add // mul_distr !T1lt_add2l yb yc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)