proposition: Lemma poly_border (p : {poly R}) a b: a < b -> (forall x, a < x < b -> 0 < p.[x]) -> 0 <= p.[a].
proof: Proof. move=> ab cp; case p0: (p.[a] < 0); last by rewrite leNgt p0. have := (cons_polyK (p \Po ('X + a%:P))); rewrite cons_poly_def. have -> : (p \Po ('X + a%:P)).[0] = p.[a]. by rewrite horner_comp hornerD hornerC hornerX add0r. move=> qdec. have : p = p \Po ('X + a%:P) \Po ('X - a%:P) by rewrite comp_polyXaddC_K. rewrite -qdec comp_polyD comp_polyC comp_polyM comp_polyX. set q := \poly_(_ < _) _; move=> pq. have [ub pu] := (poly_itv_bound (q \Po ('X - a%:P)) a b). have ub0 : 0 <= ub by rewrite (le_trans _ (pu a _)) // lexx andTb ltW. set ub' := ub + 1. have ub'0 : 0 < ub' by rewrite ltr_paddl. have ublt : ub < ub' by rewrite ltr_spaddr // ltr01. pose x := minr (a - p.[a]/ub') (half (a + b)). have xitv2 : a < x < b. by case/andP: (mid_between ab)=> A B; rewrite lt_minr ltr_spaddr ?A //= ?lt_minl ?B ?orbT // -mulNr mulr_gt0 // ?invr_gt0 // oppr_gt0. have xitv : a <= x <= b by case/andP: xitv2 => *; rewrite !ltW //. have := cp _ xitv2. rewrite [X in X.[x]]pq hornerD hornerC hornerM hornerXsubC. rewrite -[X in 0 < _ + X]opprK subr_gt0 => abs. have : x - a <= -p.[a] / ub' by rewrite ler_subl_addl le_minl mulNr lexx. rewrite -(ler_pmul2r ub'0) mulfVK; last first. by move:ub'0; rewrite lt0r=>/andP=>[[]]. have xma :0 < x - a by rewrite subr_gt0; case/andP: xitv2. move: (pu _ xitv); rewrite lter_norml; case/andP => _ {pu}. rewrite -[_ <= ub](ler_pmul2r xma) => pu2. rewrite mulrC; have := (lt_le_trans abs pu2) => {pu2} {}abs ab'. have := (le_lt_trans ab' abs); rewrite ltr_pmul2r // ltNge;case/negP. by rewrite ltW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc