proposition: Lemma sgp_right_addp0 (p q : {poly R}) x : q != 0 -> (\mu_x p > \mu_x q)%N -> sgp_right (p + q) x = sgp_right q x.
proof: Proof. move=> nq0; move hm: (\mu_x q)=> m. elim: m p q nq0 hm => [|mq ihmq] p q nq0 hmq; case hmp: (\mu_x p)=> // [mp]; do[rewrite ltnS=> hm; rewrite sgp_right_rec {1}addrC addr_eq0]. case: (eqVneq q (- p)) nq0 hmq => [-> np0 hmq|hqp nq0 hmq]. rewrite sgp_right_rec (negPf np0) -mu_gt0 // hmq ltnn /=; apply/esym/eqP. by rewrite hornerN sgrN oppr_eq0 sgr_eq0 -[_ == _]mu_gt0 ?hmp // -oppr_eq0. rewrite rootE hornerD. have ->: p.[x] = 0. apply/eqP; rewrite -[_ == _]mu_gt0 ?hmp //. by apply: contra_eq_neq hmp => ->; rewrite mu0. by rewrite [RHS]sgp_right_rec (negPf nq0) add0r -/(root _ _) -mu_gt0 // hmq. case: eqVneq => hqp. by move: hm; rewrite -ltnS -hmq -hmp hqp mu_opp ltnn. have px0: p.[x] = 0. apply/rootP; rewrite -mu_gt0 ?hmp //. by apply: contra_eq_neq hmp => ->; rewrite mu0. have qx0: q.[x] = 0 by apply/rootP; rewrite -mu_gt0 ?hmq //. rewrite rootE hornerD px0 qx0 add0r eqxx /=; symmetry. rewrite sgp_right_rec rootE (negPf nq0) qx0 eqxx /=. rewrite derivD ihmq // ?mu_deriv ?rootE ?px0 ?qx0 ?hmp ?hmq ?subn1 //. apply: contra nq0; rewrite -size_poly_eq0 size_deriv. case hsq: size=> [|sq] /=. by move/eqP: hsq; rewrite size_poly_eq0. move/eqP=> sq0; move/eqP: hsq qx0; rewrite sq0; case/size_poly1P=> c c0 ->. by rewrite hornerC; move/eqP; rewrite (negPf c0). 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)