proposition: Lemma mu_exp p x n : \mu_x (p ^+ n) = (\mu_x p * n)%N.
proof: Proof. elim: n p => [|n ihn] p; first by rewrite expr0 mu_polyC muln0. case p0: (p == 0); first by rewrite (eqP p0) exprS mul0r mu0 mul0n. by rewrite exprS mu_mul ?ihn ?mulnS// mulf_eq0 expf_eq0 p0 andbF. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)