proposition: Lemma Rolle_lim (f : R -> R) (a b : R) (h : R -> R) : (forall x : R, a < x < b \/ b < x < a -> derivable_pt_lim f x (h x)) -> (forall x : R, a <= x <= b \/ b <= x <= a -> continuity_pt f x) -> a <> b -> f a = f b -> exists c : R, (a < c < b \/ b < c < a) /\ derivable_pt_lim f c 0.
proof: Proof. intros Hd Hc hdif Heq. destruct (total_order_T a b) as [[H1|H2]|H3]. - assert (pr : forall x : R, a < x < b -> derivable_pt f x). { intros y hy. unfold derivable_pt, derivable_pt_abs. exists (h y). now apply Hd; left. } destruct (Rolle f a b pr) as [k [P HkP]]; trivial. + now intros y Hy; apply Hc; left. + exists k; split; [now left|]. now rewrite <-derive_pt_eq; apply HkP. - now destruct hdif. - assert (pr : forall x : R, b < x < a -> derivable_pt f x). { intros y hy. unfold derivable_pt, derivable_pt_abs. exists (h y). now apply Hd; right. } destruct (Rolle f b a pr) as [k [P HkP]]; trivial. + now intros y Hy; apply Hc; right. + now symmetry. + exists k; split; [now right|]. rewrite <-derive_pt_eq; apply HkP. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib