proposition: Lemma Rolle : forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x), (forall x:R, a <= x <= b -> continuity_pt f x) -> a < b -> f a = f b -> exists c : R, (exists P : a < c < b, derive_pt f c (pr c P) = 0).
proof: Proof. intros; assert (H2 : forall x:R, a < x < b -> derivable_pt id x). - intros; apply derivable_pt_id. - assert (H3 := MVT f id a b pr H2 H0 H); assert (H4 : forall x:R, a <= x <= b -> continuity_pt id x). + intros; apply derivable_continuous; apply derivable_id. + destruct (H3 H4) as (c & P & H6). exists c; exists P; rewrite H1 in H6. unfold id in H6; unfold Rminus in H6; rewrite Rplus_opp_r in H6. rewrite Rmult_0_l in H6; apply Rmult_eq_reg_l with (b - a); [ rewrite Rmult_0_r; apply H6 | apply Rminus_eq_contra; red; intro H7; rewrite H7 in H0; elim (Rlt_irrefl _ H0) ]. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra