proposition: Theorem derivable_imp_defined_ne : forall f r d u t, f (Xreal r) = Xreal u -> (u <> t)%R -> (forall v, derivable_pt_lim (proj_fun v f) r d) -> locally_true r (fun a => exists w, (w <> t)%R /\ f (Xreal a) = Xreal w).
proof: Proof. intros. apply locally_true_imp with (fun a => (exists w, f (Xreal a) = Xreal w) /\ (proj_fun 0 f a <> t)%R). intros x ((w, H2), H3). exists w. split. replace (proj_fun 0 f x) with w in H3. exact H3. unfold proj_fun. rewrite H2. apply refl_equal. exact H2. apply locally_true_and. eapply derivable_imp_defined_any ; eassumption. apply continuity_pt_ne. replace (proj_fun 0 f r) with u. exact H0. unfold proj_fun. rewrite H. apply refl_equal. apply derivable_continuous_pt. exists d. apply H1. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal