proposition: Lemma monic_Cauchy_bound : p \is monic -> {b | forall x, x >= b -> p.[x] > 0}.
proof: Proof. move/monicP=> mon_p; pose n := (size p - 2)%N. have [p_le1 | p_gt1] := leqP (size p) 1. exists 0 => x _; rewrite (size1_polyC p_le1) hornerC. by rewrite -[p`_0]lead_coefC -size1_polyC // mon_p ltr01. pose lb := \sum_(j < n.+1) `|p`_j|; exists (lb + 1) => x le_ub_x. have x_ge1: 1 <= x; last have x_gt0 := lt_le_trans ltr01 x_ge1. by rewrite -(lerD2l lb) ler_wpDl ?sumr_ge0 // => j _. rewrite horner_coef -(subnK p_gt1) -/n addnS big_ord_recr /= addn1. rewrite [in p`__]subnSK // subn1 -lead_coefE mon_p mul1r -ltrBlDl sub0r. apply: le_lt_trans (_ : lb * x ^+ n < _); last first. by rewrite exprS ltr_pM2r ?exprn_gt0// -(ltrD2r 1) ltr_pwDr. rewrite -sumrN mulr_suml ler_sum // => j _; apply: le_trans (ler_norm _) _. rewrite normrN normrM ler_wpM2l // normrX. by rewrite ger0_norm ?(ltW x_gt0) // ler_weXn2l ?leq_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)