proposition: Lemma CauchyBound : `| x | <= `|E n|^-1 * \sum_(i < n.+1) `|E i|.
proof: Proof. move: (CauchyBound2). rewrite big_distrr /=. have -> //: \sum_(i < n.+1) `|E i / E n| = \sum_(i < n.+1) (`|E n|^-1 * `|E i|). by apply: eq_bigr => i _ ; rewrite normrM normrV ? unitfE // mulrC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)