proposition: Lemma sgp_minftyP x (p : {poly R}) : {in `]-oo, x], noroot p} -> {in `]-oo, x], forall y, sgr p.[y] = sgp_minfty p}.
proof: Proof. move=> rpx y Hy; rewrite -sgp_pinfty_sym. have ->: p.[y] = (p \Po -'X).[-y] by rewrite horner_comp !hornerE opprK. apply: (@sgp_pinftyP (- x)) => /= [z Hz|]. by rewrite root_comp !hornerE rpx // in_itv /= ler_oppl (itvP Hz). by rewrite in_itv /= ler_opp2 (itvP Hy). 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)