proposition: Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) : a *? b -> f @ \oo --> a -> g @ \oo --> b -> f \* g @ \oo --> a * b.
proof: Proof. exact: cvgeM. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau