proposition: Lemma pol_cont (p : {poly R}) (x eps :R): 0 < eps -> { delta | 0 < delta & forall y, `|(y - x)| < delta -> `|p.[y] - p.[x]| < eps }.
proof: Proof. move => ep. move: (pol_ucont p (a:= x-1)(b:=x+1)); set c := _ .[_ ] => /= hc. have pa: x-1 <= x by move: (ler_add2l x (-1) 0); rewrite addr0 lerN10. have pb: x <= x+1 by move: (ler_add2l x 0 1); rewrite ler01 addr0. have cp: 0<=c. move: (hc _ _ pa pb (lexx (x+1))). by rewrite addrAC addrN add0r mulr1; apply: le_trans; rewrite normr_ge0. exists (Num.min 1 (eps /(c+1))). rewrite lt_minr ltr01 /= divr_gt0 // ? ep //. by apply: (lt_le_trans ltr01); move: (ler_add2r 1 0 c); rewrite add0r cp. move => y. rewrite lt_minr; case /andP => xy1 xy2. apply: (@le_lt_trans _ _ (c * `|(y - x)|)); last first. move: cp; rewrite le0r; case /orP; first by move /eqP => ->; rewrite mul0r. move => cp. rewrite - (ltr_pmul2l cp) in xy2; apply: (lt_le_trans xy2). rewrite mulrCA ger_pmulr //. have c1: c <= c + 1 by move: (ler_add2l c 0 1); rewrite ler01 addr0. have c1p := (lt_le_trans cp c1). by rewrite -(ler_pmul2r c1p) mulfVK ? (gt_eqF c1p) // mul1r. move: (ltW xy1); rewrite ler_distl;case /andP => le1 le2. case /orP: (le_total x y) => xy. move: (xy); rewrite - subr_ge0 => xy'. move: (hc _ _ pa xy le2). rewrite subr_ge0. rewrite -subr_ge0 in xy'. by rewrite (ger0_norm xy'). move: (xy); rewrite - subr_ge0 => xy'. move: (hc _ _ le1 xy pb); rewrite distrC (distrC y x). rewrite subr_ge0. rewrite -subr_ge0 in xy'. by rewrite (ger0_norm xy'). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)