proposition: Lemma poly_cont x p e : e > 0 -> exists2 d, d > 0 & forall y, `|y - x| < d -> `|p.[y] - p.[x]| < e.
proof: Proof. elim/(@poly_div_factor x): p e => [|p n k pxn0 Pp] e ep. by exists 1; rewrite ?ltr01// => y hy; rewrite !hornerC subrr normr0. case: (Pp (`|p.[x]|/2%:R)). by rewrite pmulr_lgt0 ?invr_gte0//= ?ltr0Sn// normrE. move=> d' d'p He'. case: (@nth_root (e / ((3%:R / 2%:R) * `|p.[x]|)) n). by rewrite ltr_pdivl_mulr ?mul0r ?pmulr_rgt0 ?invr_gt0 ?normrE ?ltr0Sn. move=> d dp rootd. exists (minr d d'); first by rewrite lt_minr dp. move=> y; rewrite lt_minr; case/andP=> hxye hxye'. rewrite !(hornerE, horner_exp) subrr expr0n mulr0n mulr0 add0r addrK normrM. apply: le_lt_trans (_ : `|p.[y]| * d ^+ n.+1 < _). by rewrite ler_wpmul2l ?normrE // normrX ler_expn2r -?topredE /= ?normrE 1?ltW. rewrite rootd mulrCA gtr_pmulr //. rewrite ltr_pdivr_mulr ?mul1r ?pmulr_rgt0 ?invr_gt0 ?ltr0Sn ?normrE //. rewrite mulrDl mulrDl divff; last by rewrite -mulr2n pnatr_eq0. rewrite !mul1r mulrC -ltr_subl_addr. by rewrite (le_lt_trans _ (He' y _)) // ler_sub_dist. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)