proposition: Lemma polyrN0_itv (i : interval R) (p : {poly R}) : {in i, noroot p} -> forall y x : R, y \in i -> x \in i -> sgr p.[x] = sgr p.[y].
proof: Proof. move=> hi y x hy hx; wlog xy: x y hx hy / x <= y. by move=> hwlog; case: (leP x y) => [|/ltW] /hwlog ->. have hxyi: (`[x, y] <= i)%O. by case: i hx hy {hi} => [bl br] /andP [hx _] /andP []; rewrite /<=%O /= hx. move: (hi _ hx) (hi _ hy); rewrite /root; do 2 case: sgrP => //. move=> /ltW py0 /ltW p0x; case: (@poly_ivt (- p) x y) => //. by rewrite !hornerN -oppr_itvcc oppr0 in_itv /= py0. by move=> z hz; rewrite rootN (negPf (hi z _)) //; apply: (le_trans hz). move=> /ltW p0y /ltW px0; case: (@poly_ivt p x y); rewrite ?in_itv /= ?px0 //=. by move=> z hz; rewrite (negPf (hi z _)) //; apply: (le_trans hz). 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)