proposition: Lemma ncvgM u v lu lv : ncvg u lu%:E -> ncvg v lv%:E -> ncvg (u \* v) (lu * lv)%:E.
proof: Proof. move=> cu cv; pose a := u \- lu%:S; pose b := v \- lv%:S. have eq: (u \* v) =1 (lu * lv)%:S \+ ((lu%:S \* b) \+ (a \* v)). move=> n; rewrite {}/a {}/b /= [u n+_]addrC [(_+_)*(v n)]mulrDl. rewrite !addrA -[LHS]add0r; congr (_ + _); rewrite mulrDr. by rewrite !(mulrN, mulNr) (addrCA (lu * lv)) subrr addr0 subrr. apply/(ncvg_eq eq); rewrite -[X in X%:E]addr0; apply/ncvgD. by apply/ncvgC. rewrite -[X in X%:E]addr0; apply/ncvgD. + apply/ncvgMr; first rewrite -[X in X%:E](subrr lv). by apply/ncvgB/ncvgC. by apply/nboundedC. + apply/ncvgMl; first rewrite -[X in X%:E](subrr lu). by apply/ncvgB/ncvgC. by apply/(ncvg_nbounded cv). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology