proposition: Lemma pol_ucont (p : {poly R}) a b (c := (norm_pol p^`()).[(Num.max (- a) b)]) : forall x y, a <= x -> x <= y -> y <= b -> `|p.[y] - p.[x]| <= c * (y - x).
proof: Proof. move => x y ax xy yb. apply: pol_lip => //. apply: (le_trans _ ax); by rewrite ler_oppl le_maxr lexx. apply: (le_trans yb); by rewrite le_maxr lexx orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)