proposition: Theorem derivable_imp_defined_any : forall f r d u, f (Xreal r) = Xreal u -> (forall v, derivable_pt_lim (proj_fun v f) r d) -> locally_true r (fun a => exists w, f (Xreal a) = Xreal w).
proof: Proof. intros. eapply derivable_imp_defined. apply H. apply Rlt_not_eq. apply Rlt_plus_1. apply H0. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal