proposition: Lemma is_lim_le_m_loc (f g : R -> R) (x : Rbar) : Rbar_locally' x (fun y => g y <= f y) -> is_lim f x m_infty -> is_lim g x m_infty.
proof: Proof. apply filterlim_le_m_infty. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq