proposition: Lemma cofactor_XsubC_mu x p n : ~~ root p x -> \mu_x (p * ('X - x%:P) ^+ n) = n.
proof: Proof. move=> p0; apply/eqP; rewrite eq_sym -muP//; last first. apply: contra p0; rewrite mulf_eq0 expf_eq0 polyXsubC_eq0 andbF orbF. by move/eqP->; rewrite root0. rewrite dvdp_mulIr /= exprS dvdp_mul2r -?root_factor_theorem //. by rewrite expf_eq0 polyXsubC_eq0 andbF //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)