proposition: Lemma MVT_cor1_pderivable : forall (pr : pderivable f (fun x => a <= x <= b)), a < b -> exists c, exists Hc : a <= c <= b, f b - f a = derive_pt f c (pr c Hc) * (b - a) /\ a < c < b.
proof: Proof. intros pr ab. have H0 : forall c : R, a < c < b -> derivable_pt f c. move=> c Hc. apply pr. 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. apply derivable_continuous_pt. apply pr. case: Hc => ? ?; lra. 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. have Hc' : a <= c <= b. clear H'. case: Hc => ? ?; lra. exists Hc'. split; last by []. 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. f_equal. by apply pr_nu. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext