proposition: Theorem Xderive_pt_partial_fun : forall g f f', (forall x y, g x = Xreal y -> f x = Xreal y) -> forall x, Xderive_pt g x f' -> Xderive_pt f x f'.
proof: Proof. intros g f f' Heq x Hg. assert (Heqx := Heq x). xtotal. now assert (H := Heqx _ (refl_equal _)). intro v. apply derivable_pt_lim_eq_locally with (2 := Hg v). apply locally_true_imp with (2 := derivable_imp_defined_any _ _ _ _ X Hg). intros x (w, Hw). unfold proj_fun. rewrite Hw. now rewrite (Heq _ _ Hw). Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal