proposition: Lemma __deprecated__ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b : (b < 0)%R -> f @ \oo --> -oo -> g @ \oo --> b%:E -> f \* g @ \oo --> +oo.
proof: Proof. move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulNye//; apply. by rewrite mule_def_infty_neq0// lt_eqF. 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