proposition: Lemma sgr_neighpr b p x : {in neighpr p x b, forall y, (sgr p.[y] = sgp_right p x)}.
proof: Proof. elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p. rewrite leqn0 size_poly_eq0 /neighpr; move/eqP=> -> /= y. by rewrite next_root0 itv_xx. rewrite leq_eqVlt ltnS; case/predU1P => [sp|]; last exact: ihn. rewrite /sgp_right sp /=; case px0: root=> /=; last first. move=> y; rewrite /neighpr => hy /=. apply/esym/(@polyrN0_itv `[x, y]) => [z||]; do ?by rewrite bound_in_itv /<=%O /= (itvP hy). rewrite (@itv_splitU _ _ (BRight x)) ?bound_lexx /<=%O /= ?(itvP hy) //. rewrite itv_xx; case/predU1P=> hz; first by rewrite hz px0. rewrite (@next_noroot p x b) //. by apply: subitvPr hz; rewrite /<=%O /= (itvP hy). have <-: size p^`() = n by rewrite size_deriv sp. rewrite -/(sgp_right p^`() x) /neighpr => y hy /=. case: (@neighpr_wit (p * p^`()) x b)=> [||m]. * case: next_rootP hy => [|? ? ? /itvP -> //|c p0 -> _]. by rewrite itv_xx. by case: leP; rewrite ?itv_xx. * rewrite mulf_neq0 //. by apply: contra_eq_neq sp => ->; rewrite size_poly0. apply: contra_eq_neq (size_deriv p) => ->; rewrite sp /=. rewrite size_poly0; apply: contraTneq px0=> hn; rewrite -hn in sp. by case/eqP/size_poly1P: sp => c nc0 ->; rewrite rootC. * rewrite neighpr_mul; case/andP=> /= hmp hmp'. rewrite (polyrN0_itv _ hmp) //; last exact: next_noroot. rewrite (@ders0r p x m (mid x m)) ?(eqP px0) ?mid_in_itv ?bound_in_itv //; rewrite /<=%O /= ?(itvP hmp) //; last first. move=> u hu /=; rewrite (@next_noroot _ x b) //. by apply: subitvPr hu; rewrite /<=%O /= (itvP hmp'). rewrite ihn ?size_deriv ?sp /neighpr //. by rewrite (subitvP _ (@mid_in_itv _ false false _ _ _)); rewrite /<=%O /= /<=%O //= ?lexx (itvP hmp'). 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)