proposition: Lemma ltr_hornerW : {in `[a, b] &, {homo horner p : x y / x < y}}.
proof: Proof. move=> x y axb ayb ltxy; have [c xcy /(canRL (@subrK _ _))->]:= mvt p ltxy. rewrite ltr_addr mulr_gt0 ?subr_gt0 ?der_pos //. 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)