proposition: Lemma ler_hornerW a b p : {in `]a, b[, forall x, p^`().[x] >= 0} -> {in `[a, b] &, {homo horner p : x y / x <= y}}.
proof: Proof. move=> der_nneg x y axb ayb; rewrite le_eqVlt => /predU1P[->//|ltxy]. have [c xcy /(canRL (@subrK _ _))->]:= mvt p ltxy. rewrite ler_addr mulr_ge0 ?subr_ge0 ?(ltW ltxy) ?der_nneg //. by apply: subitvP xcy; rewrite /<=%O /= /<=%O /= (itvP axb) (itvP ayb). 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)