proposition: Lemma Rolle (R : realType) (f : R -> R) (a b : R) : a < b -> (forall x, x \in `]a, b[%R -> derivable f x 1) -> {within `[a, b], continuous f} -> f a = f b -> exists2 c, c \in `]a, b[%R & is_derive c 1 f 0.
proof: Proof. move=> ltab fdrvbl fcont faefb. have [cmax cmaxab fcmax] := EVT_max (ltW ltab) fcont. have [cmaxeaVb|] := boolP (cmax \in [set a; b]); last first. rewrite notin_set => /not_orP[/eqP cnea /eqP cneb]. have {}cmaxab : cmax \in `]a, b[%R. by rewrite in_itv /= !lt_def !(itvP cmaxab) cnea eq_sym cneb. exists cmax => //; apply: derive1_at_max (ltW ltab) fdrvbl cmaxab _ => t tab. by apply: fcmax; rewrite in_itv /= !ltW // (itvP tab). have [cmin cminab fcmin] := EVT_min (ltW ltab) fcont. have [cmineaVb|] := boolP (cmin \in [set a; b]); last first. rewrite notin_set => /not_orP[/eqP cnea /eqP cneb]. have {}cminab : cmin \in `]a, b[%R. by rewrite in_itv /= !lt_def !(itvP cminab) cnea eq_sym cneb. exists cmin => //; apply: derive1_at_min (ltW ltab) fdrvbl cminab _ => t tab. by apply: fcmin; rewrite in_itv /= !ltW // (itvP tab). have midab : (a + b) / 2 \in `]a, b[%R by apply: mid_in_itvoo. exists ((a + b) / 2) => //; apply: derive1_at_max (ltW ltab) fdrvbl (midab) _. move=> t tab. suff fcst s : s \in `]a, b[%R -> f s = f cmax by rewrite !fcst. move=> sab. apply/eqP; rewrite eq_le fcmax; last by rewrite in_itv /= !ltW ?(itvP sab). suff -> : f cmax = f cmin by rewrite fcmin // in_itv /= !ltW ?(itvP sab). by move: cmaxeaVb cmineaVb; rewrite 2!inE => -[|] -> [|] ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms