proposition: Lemma CauchyBound_aux : x^+n = - \sum_(i < n) ((E i / E n) * x^+ i).
proof: Proof. move: xr; move /rootP => xr1. have ->: \sum_(i < n) E i / E n * x ^+ i = \sum_(i < n) (E i * x ^+ i / E n). by apply: eq_bigr => i _ ; rewrite mulrAC. rewrite -(mulfK pnz (x ^+ n)); apply /eqP; rewrite -addr_eq0 - mulr_suml. rewrite - mulrDl mulf_eq0 -{2} xr1; apply /orP; left. by rewrite horner_poly (big_ord_recr n) //= addrC mulrC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)