proposition: Lemma is_lim_ext (f g : R -> R) (x l : Rbar) : (forall y, f y = g y) -> is_lim f x l -> is_lim g x l.
proof: Proof. move => H. apply is_lim_ext_loc. by apply filter_forall. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq