proposition: Lemma filterdiff_ext_locally (f g : U -> V) (x : U) (l : U -> V) : locally x (fun y => f y = g y) -> filterdiff f (locally x) l -> filterdiff g (locally x) l.
proof: Proof. move => H. apply filterdiff_ext_loc with (1 := H). move => y Hy. destruct H as [d Hd]. apply Hd. replace y with x. apply ball_center. by apply is_filter_lim_locally_unique. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv