proposition: Lemma ex_derive_continuous (f : K -> V) (x : K) : ex_derive f x -> continuous f x.
proof: Proof. intros. apply @filterdiff_continuous. by apply ex_derive_filterdiff. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv