proposition: Lemma sgp_pinftyP x (p : {poly R}) : {in `[x , +oo[, noroot p} -> {in `[x, +oo[, forall y, sgr p.[y] = sgp_pinfty p}.
proof: Proof. rewrite /sgp_pinfty; wlog lp_gt0 : x p / lead_coef p > 0 => [hwlog|rpx y Hy]. have [|/(hwlog x p) //|/eqP] := ltrgtP (lead_coef p) 0; last first. by rewrite lead_coef_eq0 => /eqP -> ? ? ?; rewrite lead_coef0 horner0. rewrite -[p]opprK lead_coefN oppr_cp0 => /(hwlog x _) Hp HNp y Hy. by rewrite hornerN !sgrN Hp => // z /HNp; rewrite rootN. have [z Hz] := poly_pinfty_gt_lc lp_gt0. have {}Hz u : u \in `[z, +oo[ -> Num.sg p.[u] = 1. rewrite in_itv andbT => /Hz pu_ge1. by rewrite gtr0_sg // (lt_le_trans lp_gt0). rewrite (@polyrN0_itv _ _ rpx (maxr y z)) ?in_itv /= ?le_maxr ?(itvP Hy) //. by rewrite Hz ?gtr0_sg // in_itv /= le_maxr lexx orbT. 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)