proposition: Lemma cauchy_boundP (p : {poly R}) x : p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p.
proof: Proof. move=> np0 rpx; rewrite ltr_spaddl ?ltr01 //. case e: (size p) => [|n]; first by move: np0; rewrite -size_poly_eq0 e eqxx. have lcp : `|lead_coef p| > 0 by move: np0; rewrite -lead_coef_eq0 -normr_gt0. case: (lerP `|x| 1) => cx1. rewrite (le_trans cx1) // ler_pdivl_mull // mulr1. by rewrite big_ord_recr /= /lead_coef e ler_addr sumr_ge0. have xp : 0 < `|x| by rewrite (lt_trans _ cx1) ?ltr01. rewrite ler_pdivl_mull // /lead_coef e /= big_ord_recr /= ler_paddr //. case es: n e => [|m] e. by move: rpx np0; rewrite (@size1_polyC _ p) ?e // hornerC => -> /eqP. have/ler_pmul2r <-: 0 < `|x| ^+ m by rewrite exprn_gt0. rewrite -mulrA -exprS -(normrX m.+1) -normrM -es big_distrl /=. apply: le_trans (_ : \sum_(i < n) `|p`_i * x ^+ i| <= _). move/eqP: rpx; rewrite horner_coef e -es big_ord_recr /= addrC addr_eq0. by move/eqP ->; rewrite normrN ler_norm_sum. rewrite es; apply: ler_sum => i _. by rewrite normrM normrX ler_pmul ?exprn_ge0 // ler_eexpn2l // leq_ord. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)