proposition: Lemma Derive_ext_loc : forall f g x, locally x (fun t => f t = g t) -> Derive f x = Derive g x.
proof: Proof. intros f g x Hfg. rewrite /Derive /Lim. apply f_equal, Lim_seq_ext_loc. apply (filterlim_Rbar_loc_seq 0 (fun h => (f (x + h) - f x) / h = (g (x + h) - g x) / h)). apply (filter_imp (fun h => f (x + h) = g (x + h))). intros h ->. by rewrite (locally_singleton _ _ Hfg). destruct Hfg as [eps He]. exists eps => h H Hh. apply He. rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /=. now replace (x + h + - x) with (h - 0) by ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv