proposition: Lemma mu_gcdp_eq1 : forall (p : {poly R}) (x : R), (p != 0) -> root p x -> (\mu_x (divp p (gcdp p p^`())) == 1)%N.
proof: Proof. move=> p x Hp zero_x. rewrite -(@eqn_add2r ((\mu_x)%R p)) (@addnC 1%N _) addn1 -{1}(@prednK ((\mu_x)%R p)) ?mu_gt0 //. rewrite addnS -(eqP (mu_x_gcdp Hp zero_x)) -mu_mul. rewrite divpK ?mu_mulC //; last by apply dvdp_gcdl. by apply lc_expn_scalp_neq0. rewrite divpK. rewrite -size_poly_gt0 -mul_polyC size_Cmul ?size_poly_gt0 //. by apply lc_expn_scalp_neq0. by apply dvdp_gcdl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)