proposition: Lemma cm3 {R : realFieldType} (b : R) : (0 < b)%R -> forall l : {poly R}, {c | forall x y : R, (0 <= x)%R -> (x <= y)%R -> (y <= b)%R -> `|l.[y] - l.[x]| <= c * (y - x)}.
proof: Proof. move=> pb; elim/poly_ind=> [ | l u [c cp]]. by exists 0%R => x y; rewrite !hornerE oppr0 normr0 lexx. exists ((\sum_(i < size l) `|nth 0 l i| * b ^+ i) + c * b). move=> x y xge0 xy yb. rewrite !hornerE addrAC opprD addrA addrNK. rewrite [A in `|A|](_ : _ = l.[y] * y - l.[y] * x + l.[y] * x - l.[x] * x); last by rewrite -[_ - _ + _]addrA addNr addr0. have py : (0 <= y)%R by rewrite (le_trans xge0). have psyx : (0 <= y - x)%R by rewrite subr_ge0. rewrite -addrA (le_trans (ler_norm_add _ _)) //. rewrite -mulrBr -mulrBl !normrM (ger0_norm xge0) (ger0_norm psyx). rewrite [X in _ <= X]mulrDl ler_add//. rewrite ler_wpmul2r// (le_trans (ler_horner_norm_pol l y py))//. apply: ler_sum => i _. rewrite ler_wpmul2l ?normr_ge0//. by rewrite ler_expn2r// nnegrE (le_trans _ yb). rewrite mulrAC ler_pmul//; first exact: cp. by rewrite (le_trans xy). Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc