proposition: Lemma sgr_neighprN p x b : p.[x] != 0 -> {in neighpr p x b, forall y, (sgr p.[y] = sgr p.[x])}.
proof: Proof. rewrite /neighpr=> nrpx /= y hy; symmetry. apply: (@polyrN0_itv `[x, y]); do ?by rewrite bound_in_itv /<=%O /= (itvP hy). move=> z; rewrite (@itv_splitU _ _ (BRight x)) ?itv_xx /=; last first. by rewrite bound_lexx /<=%O /= (itvP hy). case/predU1P => [-> //|hz]; rewrite (@next_noroot _ x b) //. by apply: subitvPr 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)