proposition: Lemma MVT_cor1_pderivable_closed_continuity f a b : forall (prd : pderivable f (fun x => a < x < b)) (prc : forall x (Hx : a <= x <= b), continuity_pt f x), a < b -> exists c (Hc : a < c < b), f b - f a = derive_pt f c (prd c Hc) * (b - a) /\ a < c < b.
proof: Proof. intros prd prc ab. have H0 : forall c : R, a < c < b -> derivable_pt f c. move=> c Hc. apply prd. case: Hc => ? ?; lra. have H1 : forall c : R, a < c < b -> derivable_pt id c. move=> c _; by apply derivable_pt_id. have H2 : forall c, a <= c <= b -> continuity_pt f c. move=> x Hc. by apply prc. have H3 : forall c, a <= c <= b -> continuity_pt id c. move=> x Hc; by apply derivable_continuous_pt, derivable_pt_id. case: (MVT f id a b H0 H1 ab H2 H3) => c [Hc H']. exists c. exists Hc. split => //. cut (derive_pt id c (H1 c Hc) = derive_pt id c (derivable_pt_id c)); [ intro | apply pr_nu ]. rewrite H (derive_pt_id c) mulR1 in H'. rewrite -H' /= /id mulRC. congr (_ * _). exact: pr_nu. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext