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