proposition: Lemma sgr_neighplN p a x : ~~ root p x -> {in neighpl p a x, forall y, (sgr p.[y] = sgr p.[x])}.
proof: Proof. rewrite /neighpl=> nrpx /= y hy. apply: (@polyrN0_itv `[y, x]); do ?by rewrite bound_in_itv /<=%O /= (itvP hy). move=> z; rewrite (@itv_splitU _ _ (BLeft x)) ?itv_xx /=; last first. by rewrite bound_lexx /<=%O /= (itvP hy). rewrite orbC => /predU1P[-> // | hz]. rewrite (@prev_noroot _ a x) //. by apply: subitvPl hz; rewrite /<=%O /= (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)