proposition: Lemma ncvgMr u v : ncvg v 0%:E -> nbounded u -> ncvg (u \* v) 0%:E.
proof: Proof. move=> cv bu; apply/(@ncvg_eq (v \* u)). by move=> x; rewrite /= mulrC. by apply/ncvgMl. 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