proposition: Theorem Xderive_MVT : forall f f', Xderive f f' -> forall dom : R -> Prop, connected dom -> (forall x, dom x -> f' (Xreal x) <> Xnan) -> forall m, dom m -> forall x, dom x -> exists c, dom c /\ f (Xreal x) = Xadd (f (Xreal m)) (Xmul (f' (Xreal c)) (Xsub (Xreal x) (Xreal m))).
proof: Proof. intros f f' Hd dom Hdom Hf'. set (fr := proj_fun 0 f). set (fr' := proj_fun 0 f'). unfold Xderive, Xderive_pt in Hd. assert (R1: forall x, dom x -> f (Xreal x) = Xreal (fr x)). intros x Hx. generalize (Hd (Xreal x)) (Hf' x Hx). unfold fr, proj_fun at 2. case (f' (Xreal x)). intros _ H. elim H. apply refl_equal. case (f (Xreal x)). intros _ H _. elim H. intros r _ _ _. apply refl_equal. assert (R2: forall x, dom x -> f' (Xreal x) = Xreal (fr' x)). intros x Hx. generalize (Hd (Xreal x)) (Hf' x Hx). unfold fr', proj_fun at 2. case (f' (Xreal x)). intros _ H. elim H. apply refl_equal. intros r _ _. apply refl_equal. assert (H9: forall u v, dom u -> dom v -> (u < v)%R -> exists c, dom c /\ f (Xreal v) = Xadd (f (Xreal u)) (Xmul (f' (Xreal c)) (Xsub (Xreal v) (Xreal u)))). intros u v Hu Hv Huv. destruct (MVT_cor3 fr fr' u v Huv) as [c [P1 [P2 P3]]]. intros c Hc1 Hc2. assert (Hc := Hdom _ _ Hu Hv _ (conj Hc1 Hc2)). generalize (Hd (Xreal c)). rewrite (R2 _ Hc), (R1 _ Hc). intro H2. exact (H2 R0). exists c. assert (Hc := Hdom _ _ Hu Hv _ (conj P1 P2)). split. exact Hc. rewrite (R2 _ Hc), (R1 _ Hu), (R1 _ Hv). simpl. apply f_equal. exact P3. intros m Hm x Hx. destruct (total_order_T m x) as [[H|H]|H]. now apply (H9 m x). exists m. split. exact Hm. rewrite H, (R1 _ Hx), (R2 _ Hx). simpl. apply f_equal. ring. destruct (H9 x m Hx Hm H) as (c, (Hc, H0)). exists c. split. exact Hc. rewrite H0. rewrite (R2 _ Hc), (R1 _ Hx). simpl. apply f_equal. ring. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal