proposition: Lemma sgp_right_mod p q x : (\mu_x p < \mu_x q)%N -> sgp_right (rmodp p q) x = (sgr (lead_coef q)) ^+ (rscalp p q) * sgp_right p x.
proof: Proof. case: (eqVneq p 0) => [-> _|p0 mupq]; first by rewrite rmod0p !sgp_right0 mulr0. have qn0 : q != 0 by apply: contraTneq mupq => ->; rewrite -leqNgt mu0. move/(canLR (addKr _)): (rdivp_eq q p) => <-. have [->|qpq0] := eqVneq (rdivp p q) 0. by rewrite mul0r oppr0 add0r sgp_right_scale // sgrX. rewrite sgp_right_addp0 ?sgp_right_scale ?sgrX //. by rewrite scaler_eq0 negb_or p0 lcn_neq0. by rewrite mu_mulC ?lcn_neq0 // mu_opp mu_mul ?mulf_neq0 ?qpq0 // ltn_addl. 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)