proposition: Lemma ex_derive_ext : forall (f g : K -> V) (x : K), (forall t : K, f t = g t) -> ex_derive f x -> ex_derive g x.
proof: Proof. intros f g x Heq [l Hf]. exists l ; move: Hf ; by apply is_derive_ext. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv