proposition: Lemma ncvgMl u v : ncvg u 0%:E -> nbounded v -> ncvg (u \* v) 0%:E.
proof: Proof. move=> cu /asboolP/nboundedP [M gt0_M ltM]; elim/nbh_finW => e /= gt0_e. case: (cu (B 0 (e / (M + 1)))) => K {}cu; exists K => n le_Kn. rewrite inE subr0 normrM; apply/(@lt_trans _ _ (e / (M + 1) * M)). apply/ltr_pM => //; have /cu := le_Kn; rewrite inE subr0 eclamp_id //. by rewrite mulr_gt0 // invr_gt0 addr_gt0. rewrite -mulrAC -mulrA gtr_pMr // ltr_pdivrMr ?addr_gt0 //. by rewrite mul1r ltrDl. 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