proposition: Lemma pol_lip p (z x y: R): -z <= x -> x <= y -> y <= z -> `|(p.[y] - p.[x])| <= (norm_pol p^`()).[z] * (y - x).
proof: Proof. move => zx xy yz. rewrite horner_poly !horner_coef - sumrB. apply: (@le_trans _ _ (\sum_(i<size p) `|(p`_i * y ^+ i - p`_i * x ^+ i)|)). apply: ler_norm_sum. set aux := (X in _ <= X). have ->: aux = ((\sum_(i<size p) `|p`_i| * (z^+(i.-1) *+ i)) * (y - x)). congr(_ * _); case (poly0Vpos p). by move => ->; rewrite deriv0 size_poly0 !big_ord0. move => s1; rewrite - (prednK s1) size_deriv big_ord_recl mulr0n mulr0 add0r. apply: eq_bigr => i _; rewrite coef_deriv normrMn mulrnAl mulrnAr //. rewrite big_distrl /= ler_sum // => i _;rewrite - mulrBr normrM -mulrA. apply: (ler_wpmul2l (normr_ge0 p`_i)); exact: (diff_xn_ub i zx xy yz). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)