proposition: Lemma ex_derive_ext_loc : forall (f g : K -> V) (x : K), locally x (fun t : K => f t = g t) -> ex_derive f x -> ex_derive g x.
proof: Proof. intros f g x Hfg (l,Hf). exists l. apply: is_derive_ext_loc Hfg Hf. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv