proposition: Lemma Lim_ext_loc (f g : R -> R) (x : Rbar) : Rbar_locally' x (fun y => f y = g y) -> Lim g x = Lim f x.
proof: Proof. move => H. apply sym_eq. apply Lim_seq_ext_loc. apply: filterlim_Rbar_loc_seq H. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq