proposition: Theorem rolle a b p : a < b -> p.[a] = p.[b] -> {c | c \in `]a, b[ & p^`().[c] = 0}.
proof: Proof. move=> lab pab. wlog pb0 : p pab / p.[b] = 0. case/(_ (p - p.[b]%:P)); rewrite ?hornerE ?pab ?subrr //. by move=> c acb; rewrite derivE derivC subr0 => hc; exists c. move: pab; rewrite pb0=> pa0. have: forall rs : seq R, {subset rs <= `]a, b[} -> (size p <= size rs)%N -> uniq rs -> all (root p) rs -> p = 0. by move=> rs hrs; apply: poly_ltsp_roots. elim: (size p) a b lab pa0 pb0=> [|n ihn] a b lab pa0 pb0 max_roots. rewrite (@max_roots [::]) //=. by exists (mid a b); rewrite ?mid_in_itv // derivE horner0. case: (@rolle_weak a b p); rewrite // ?pa0 ?pb0 //=. move=> c hc; case: eqVneq => p'c0 pc0; first by exists c. suff: { d : R | d \in `]a, c[ & (p^`()).[d] = 0 }. case=> [d hd] p'd0; exists d=> //. by apply: subitvPr hd; rewrite /<=%O /= (itvP hc). apply: ihn => //; [by rewrite (itvP hc) | exact/eqP |]. move=> rs hrs srs urs rrs; apply: (max_roots (c :: rs))=> //=; last exact/andP. move=> x; rewrite in_cons; case/predU1P=> [-> //|hx]. by apply: subitvPr (hrs _ _); rewrite /<=%O //= (itvP hc). by rewrite urs andbT; apply/negP; move/hrs; rewrite bound_in_itv. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)