proposition: Lemma CauchyBound1 : `| x | <= 1 + \max_(i < n) (`|E i / E n|).
proof: Proof. move: (bigmaxf_ge0 (fun i => `|E i / E n|) n) => cp. case: (lerP `|x| 1)=> cx1; first by rewrite ler_paddr //. rewrite addrC -ler_subl_addr. move: (normr_sumprod (fun i => E i / E n) (fun i => x ^+ i) n). move: CauchyBound_aux => eq; move: (f_equal (fun z => `| z |) eq). rewrite normrN; move => <-; have ->: \sum_(i < n) `|x ^+ i| = (\sum_(i < n) `|x| ^+ i). by apply: eq_big => // i _; rewrite normrX. move: cp. case:n => [| m]; first by rewrite big_ord0 mulr0 expr0 normr1 ler10. move: (sum_powers_of_x (m.+1) `|x|); set aux:= (\sum_(i < m.+1) _) => pa. set c := \max_(i < m.+1) `|E i / E m.+1| => cp r1. have a1p: 0 < `|x| - 1 by rewrite subr_gt0. have r2 : c* aux <= c* ( (`|x| ^+ m.+1) /(`|x| - 1)). by rewrite (ler_wpmul2l cp) // ler_pdivl_mulr // mulrC pa ger_addl lerN10. move: (le_trans r1 r2); rewrite mulrA ler_pdivl_mulr // mulrC. rewrite normrX ler_pmul2r //. by apply:(lt_trans ltr01); rewrite exprn_egt1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)