proposition: Lemma ex_lim_ext_loc (f g : R -> R) (x : Rbar) : Rbar_locally' x (fun y => f y = g y) -> ex_lim f x -> ex_lim g x.
proof: Proof. move => H [l Hf]. exists l. by apply is_lim_ext_loc with f. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq