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