proposition: Lemma ex_filterdiff_ext_locally (f g : U -> V) x : locally x (fun y => f y = g y) -> ex_filterdiff f (locally x) -> ex_filterdiff g (locally x).
proof: Proof. intros H [l Hl]. exists l ; by apply filterdiff_ext_locally with f. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv