proposition: Lemma MVT_unusable : forall a', open_interval a b a' -> forall x y : R, open_interval a a' x -> open_interval a a' y -> x < y -> exists c : R, exists Hopenc : open_interval a b c, (f y - f x) * derive_pt g c (Dg c Hopenc) = derive_pt f c (Df c Hopenc) * (g y - g x) /\ x < c < y.
proof: Proof. intros a' Hopennew. generalize MVT. intros. specialize (H f g x y). assert (forall c, x < c < y -> derivable_pt f c). intros. apply Df. unfold open_interval in *. split. now apply Rlt_trans with x ; intuition. apply Rlt_trans with y ; intuition. now apply Rlt_trans with a'; intuition. assert (forall c, x < c < y -> derivable_pt g c). intros. apply Dg. unfold open_interval in *. split. now apply Rlt_trans with x ; intuition. apply Rlt_trans with y ; intuition. now apply Rlt_trans with a'; intuition. specialize (H H3 H4 H2). assert (forall c : R, x <= c <= y -> continuity_pt f c). intros. apply Cf. unfold open_interval in *. split. now apply Rle_trans with x; intuition. apply Rle_trans with y; intuition. now apply Rle_trans with a'; intuition. assert (forall c : R, x <= c <= y -> continuity_pt g c). intros. apply Cg. unfold open_interval in *. split. now apply Rle_trans with x; intuition. apply Rle_trans with y; intuition. now apply Rle_trans with a'; intuition. specialize (H H5 H6). destruct H as [c [P Hold2]]. exists c. assert (Hopenc : open_interval a b c). unfold open_interval in *. destruct P; split. now apply Rlt_trans with x; intuition. apply Rlt_trans with y; intuition. now apply Rlt_trans with a'; intuition. exists Hopenc. split. rewrite (pr_nu f c _ (H3 c P)). rewrite (pr_nu g c _ (H4 c P)). rewrite <- Hold2. now ring. apply P. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality