proposition: Lemma mu_deriv : forall x (p : {poly R}), root p x -> \mu_x (p^`()) = (\mu_x p - 1)%N.
proof: Proof. move=> x p px0; have [-> | nz_p] := eqVneq p 0; first by rewrite derivC mu0. have [q nz_qx Dp] := mu_spec x nz_p. case Dm: (\mu_x p) => [|m]; first by rewrite Dp Dm mulr1 (negPf nz_qx) in px0. rewrite subn1 Dp Dm !derivCE exprS mul1r mulrnAr -mulrnAl mulrA -mulrDl. rewrite cofactor_XsubC_mu // rootE !(hornerE, hornerMn) subrr mulr0 add0r. by rewrite mulrn_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)