proposition: Theorem derivable_imp_defined_any_2 : forall f1 f2 r d1 d2 u1 u2, f1 (Xreal r) = Xreal u1 -> f2 (Xreal r) = Xreal u2 -> (forall v, derivable_pt_lim (proj_fun v f1) r d1) -> (forall v, derivable_pt_lim (proj_fun v f2) r d2) -> locally_true r (fun a => (exists w1, f1 (Xreal a) = Xreal w1) /\ (exists w2, f2 (Xreal a) = Xreal w2)).
proof: Proof. intros. apply locally_true_and. apply (derivable_imp_defined_any _ _ _ _ H H1). apply (derivable_imp_defined_any _ _ _ _ H0 H2). Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal