proposition: Lemma root_mu p x : ('X - x%:P) ^+ (\mu_x p) %| p.
proof: Proof. case p0: (p == 0); first by rewrite (eqP p0) mu0 expr0 dvd1p. case: (@mu_spec p x); first by rewrite p0. by move=> q qn0 hp //=; rewrite {2}hp dvdp_mulIr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)