proposition: Theorem derivable_imp_defined : forall f r d u v, f (Xreal r) = Xreal u -> u <> 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. assert (continuity_pt (proj_fun v f) r). apply derivable_continuous_pt. exists d. exact H1. clear H1. replace u with (proj_fun v f r) in H0. destruct (continuity_pt_ne _ _ _ H0 H2) as (delta, (Hdelta, H3)). exists delta. split. exact Hdelta. intros. generalize (H3 _ H1). unfold proj_fun. case (f (Xreal (r + h))). intro H4. elim H4. apply refl_equal. intros. exists r0. apply refl_equal. unfold proj_fun. rewrite H. apply refl_equal. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal