proposition: Lemma Cauchy_root_bound p : p != 0 -> {b | forall x, root p x -> `|x| <= b}.
proof: Proof. move=> nz_p; set a := lead_coef p; set n := (size p).-1. have [q Dp]: {q | forall x, x != 0 -> p.[x] = (a - q.[x^-1] / x) * x ^+ n}. exists (- \poly_(i < n) p`_(n - i.+1)) => x nz_x. rewrite hornerN mulNr opprK horner_poly mulrDl !mulr_suml addrC. rewrite horner_coef polySpred // big_ord_recr (reindex_inj rev_ord_inj) /=. rewrite -/n -lead_coefE; congr (_ + _); apply: eq_bigr=> i _. by rewrite exprB ?unitfE // -exprVn mulrA mulrAC exprSr mulrA. have [b ub_q] := poly_disk_bound q 1; exists (b / `|a| + 1) => x px0. have b_ge0: 0 <= b by rewrite (le_trans (normr_ge0 q.[1])) ?ub_q ?normr1. have{b_ge0} ba_ge0: 0 <= b / `|a| by rewrite divr_ge0. rewrite real_leNgt ?rpredD ?rpred1 ?ger0_real //. apply: contraL px0 => lb_x; rewrite rootE. have x_ge1: 1 <= `|x| by rewrite (le_trans _ (ltW lb_x)) // ler_wpDl. have nz_x: x != 0 by rewrite -normr_gt0 (lt_le_trans ltr01). rewrite {}Dp // mulf_neq0 ?expf_neq0 // subr_eq0 eq_sym. have: (b / `|a|) < `|x| by rewrite (lt_trans _ lb_x) // ltr_pwDr ?ltr01. apply: contraTneq => /(canRL (divfK nz_x))Dax. rewrite ltr_pdivrMr ?normr_gt0 ?lead_coef_eq0 // mulrC -normrM -{}Dax. by rewrite le_gtF // ub_q // normfV invf_le1 ?normr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)