proposition: Lemma ex_filterdiff_ext_loc {F} {FF : Filter F} (f g : U -> V) : F (fun y => f y = g y) -> (forall x, is_filter_lim F x -> f x = g x) -> ex_filterdiff f F -> ex_filterdiff g F.
proof: Proof. intros H H0 [l Hl]. exists l ; by apply filterdiff_ext_loc with f. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv