proposition: Lemma is_derive_ext_alt f g x (f' : R -> R) (P : R -> Prop) : P x -> open P -> (forall t : R, P t -> f t = g t) -> (forall t : R, P t -> is_derive f t (f' t)) -> is_derive g x (f' x).
proof: Proof. move=> Hx HP Hfg Hf. apply: (is_derive_ext_loc f); last exact: Hf. exact: (@locally_open _ P _ HP Hfg). Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp