proposition: Lemma mu_x_gcdp : forall (p : {poly R}) (x : R), (p != 0) -> (root p x) -> \mu_x (gcdp p p^`()) == (\mu_x p) .-1.
proof: Proof. move=> p x Hp zero_x. have [q Hq Hpp] := (@mu_spec R p x Hp). have Hmu : ((\mu_x p)%R > 0)%N by rewrite mu_gt0. have Hpderiv : (deriv p) = ('X - x%:P) ^+ (\mu_x p).-1 * ((\mu_x p)%:R *: q + ('X-x%:P) * (deriv q)). by rewrite mulrDr mulrA -exprSr prednK // -scalerCA -derivXsubCexpn // -derivM mulrC {1}Hpp. rewrite eq_sym -muP. apply/andP; split. rewrite dvdp_gcd. apply/andP; split. by rewrite {2}Hpp -(@prednK (\mu_x p)) // exprS mulrA; apply dvdp_mulIr. by rewrite Hpderiv; apply dvdp_mulIl. rewrite prednK // dvdp_gcd negb_and. apply/orP; right. rewrite Hpderiv -{1}(@prednK (\mu_x p)) // exprSr dvdp_mul2l. rewrite dvdp_addl; last by apply dvdp_mulr. rewrite (@eqp_dvdr _ q ((\mu_x p)%:R *: q) ('X -x%:P)). by rewrite dvdp_XsubCl. apply eqp_scale. have/charf0P ->:= HR. by rewrite -lt0n //. by rewrite -size_poly_gt0 size_exp_XsubC prednK //. by rewrite gcdp_eq0 negb_and Hp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)