proposition: Lemma ex_filterdiff_locally {F} {FF : ProperFilter F} (f : U -> V) x : is_filter_lim F x -> ex_filterdiff f (locally x) -> ex_filterdiff f F.
proof: Proof. intros Fx [l Df]. eexists. apply filterdiff_locally with x. by []. by apply Df. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv