proposition: Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) : (forall n, 0 <= f n) -> f @ \oo --> a -> 0 <= a.
proof: Proof. by move=> f_ge0; apply: cvge_ge; apply: nearW. 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