proposition: Lemma MVT_cor1 : forall (f:R -> R) (a b:R) (pr:derivable f), a < b -> exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b.
proof: Proof. intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c); [ intro X | intros; apply pr ]. cut (forall c:R, a < c < b -> derivable_pt id c); [ intro X0 | intros; apply derivable_pt_id ]. cut (forall c:R, a <= c <= b -> continuity_pt f c); [ intro | intros; apply derivable_continuous_pt; apply pr ]. cut (forall c:R, a <= c <= b -> continuity_pt id c); [ intro | intros; apply derivable_continuous_pt; apply derivable_id ]. assert (H2 := MVT f id a b X X0 H H0 H1). destruct H2 as (c & P & H4). exists c; split. - cut (derive_pt id c (X0 c P) = derive_pt id c (derivable_pt_id c)); [ intro H5 | apply pr_nu ]. rewrite H5 in H4; rewrite (derive_pt_id c) in H4; rewrite Rmult_1_r in H4; rewrite <- H4; replace (derive_pt f c (X c P)) with (derive_pt f c (pr c)); [ idtac | apply pr_nu ]; apply Rmult_comm. - apply P. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra