proposition: Lemma poly_disk_bound p b : {ub | forall x, `|x| <= b -> `|p.[x]| <= ub}.
proof: Proof. exists (\sum_(j < size p) `|p`_j| * b ^+ j) => x le_x_b. rewrite horner_coef (le_trans (ler_norm_sum _ _ _)) ?ler_sum // => j _. rewrite normrM normrX ler_wpM2l ?lerXn2r ?unfold_in //=. exact: le_trans (normr_ge0 x) le_x_b. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)