proposition: Theorem mvt a b p : a < b -> {c | c \in `]a, b[ & p.[b] - p.[a] = p^`().[c] * (b - a)}.
proof: Proof. move=> lab. pose q := (p.[b] - p.[a])%:P * ('X - a%:P) - (b - a)%:P * (p - p.[a]%:P). case: (@rolle a b q) => // [|c lacb q'x0]. by rewrite !hornerE !subrr !mulr0 mulrC !subrr. exists c=> //; move/eqP: q'x0; rewrite !derivE !(mul0r,add0r,subr0,mulr1). by rewrite !hornerE mulrC subr_eq0; move/eqP. 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)