proposition: Theorem Xderive_pt_eq_fun : forall g f f', (forall x, f x = g x) -> forall x, Xderive_pt g x f' -> Xderive_pt f x f'.
proof: Proof. intros g f f' Heq x Hg. apply Xderive_pt_partial_fun with (2 := Hg). intros. now rewrite Heq. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal