proposition: Lemma poly_itv_bound a b : {ub | forall x, a <= x <= b -> `|p.[x]| <= ub}.
proof: Proof. have [ub le_p_ub] := poly_disk_bound p (Num.max `|a| `|b|). exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // le_max !ler_normr. by have [_|_] := ler0P x; rewrite ?lerN2 ?le_a_x ?le_x_b orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)