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