proposition: Lemma sgr_neighpl a p x : {in neighpl p a x, forall y, (sgr p.[y] = (-1) ^+ (odd (\mu_x p)) * sgp_right p x) }.
proof: Proof. elim: (size p) {-2}p (leqnn (size p))=> [|n ihn] {}p. rewrite leqn0 size_poly_eq0 /neighpl; move/eqP=> -> /= y. by rewrite prev_root0 itv_xx. rewrite leq_eqVlt ltnS; case/predU1P => [sp y|]; last exact: ihn. rewrite /sgp_right sp /=; case px0: root=> /=; last first. rewrite /neighpl => hy /=; symmetry. move: (negbT px0); rewrite -mu_gt0; last first. by apply: contraFneq px0 => ->; rewrite rootC. rewrite -leqNgt leqn0; move/eqP ->; rewrite /= expr0 mul1r. apply/esym/(@polyrN0_itv `[y, x]) => [z||]; do ?by rewrite bound_in_itv /<=%O /= (itvP hy). rewrite (@itv_splitU _ _ (BLeft x)) ?bound_lexx /<=%O /= ?(itvP hy) //. rewrite itv_xx /= orbC; case/predU1P=> [->|hz]; first by rewrite px0. rewrite (@prev_noroot p a x) //. by apply: subitvPl hz; rewrite /<=%O /= (itvP hy). have <-: size p^`() = n by rewrite size_deriv sp. rewrite -/(sgp_right p^`() x) /neighpl=> hy /=. case: (@neighpl_wit (p * p^`()) a x)=> [||m]. * case: prev_rootP hy; first by rewrite itv_xx. by move=> ? ? ? /itvP ->. by move=> c p0 -> _; case: ltP; 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 neighpl_mul; case/andP=> /= hmp hmp'. rewrite (polyrN0_itv _ hmp) //; last exact: prev_noroot. rewrite (@ders0l p m x (mid m x)) ?(eqP px0) ?mid_in_itv ?bound_in_itv; rewrite /<=%O //= ?(itvP hmp) //; last first. move=> u hu /=; rewrite (@prev_noroot _ a x) //. by apply: subitvPl hu; rewrite /<=%O /= (itvP hmp'). rewrite ihn ?size_deriv ?sp /neighpl //; last first. by rewrite (subitvP _ (@mid_in_itv _ true true _ _ _)); rewrite /<=%O /= /<=%O //= ?lexx (itvP hmp'). rewrite mu_deriv // oddB ?mu_gt0 //=; last by rewrite -size_poly_eq0 sp. by rewrite signr_addb /= mulrN1 mulNr opprK. 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)