proposition: Lemma filterdiff_continuous (f : U -> V) x : ex_filterdiff f (locally x) -> continuous f x.
proof: Proof. intros. by apply filterdiff_continuous_aux. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv