proposition: Lemma CauchyBound2 : `| x | <= \sum_(i < n.+1) `|E i / E n|.
proof: Proof. case: (lerP `|x| 1)=> cx1. apply: (le_trans cx1). rewrite big_ord_recr /= divff // normr1 ler_addr. rewrite sumr_ge0 // => i _; rewrite absr_ge0 //. move: (CauchyBound_aux). case e: n=> [| m]. by rewrite expr0 big_ord0 oppr0; move /eqP; rewrite oner_eq0. case x0 : (x == 0). by move: cx1; rewrite (eqP x0) normr0 ltr10. have xmn0 : (x^+m != 0) by rewrite expf_eq0 x0 andbF. move => h1; have h2 : x = - \sum_(i < m.+1) ( x^-(m - i) *(E i / E m.+1)). apply: (mulIf xmn0); rewrite mulNr big_distrl /= -exprS h1; congr (- _). apply: congr_big; [by [] | by [] |] => [[i hi]] _ /=. have mi : m = (m - i + i)%N by rewrite subnK //. by rewrite (mulrC (x ^-(m -i)) _) {4} mi exprD -!mulrA mulKf // expf_eq0 x0 andbF. rewrite (f_equal (fun z => `| z |) h2) normrN. apply: le_trans (_: (\sum_(i < m.+1) `|E i / E m.+1|) <= _); last first. by rewrite (big_ord_recr m.+1) /= ler_addl normr_ge0. have pa: (forall i, (i<m.+1)%N -> `| x ^- (m - i) | <= 1). move => i lin. have pa: 0 < `|x ^+ (m - i)| by rewrite normr_gt0 expf_eq0 x0 andbF. rewrite normrV. rewrite invr_le1 //; last by apply: unitf_gt0. rewrite normrX; apply:exprn_ege1; exact (ltW cx1). by apply: unitrX; rewrite unitfE x0. rewrite - [\sum_(i < m.+1) `|E i / E m.+1| ] mul1r. exact :(normr_sumprod1 (fun i => E i / E m.+1) ler01 pa). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)