proposition: Lemma mu_div p x n : (n <= \mu_x p)%N -> \mu_x (p %/ ('X - x%:P) ^+ n) = (\mu_x p - n)%N.
proof: Proof. move=> hn. case p0: (p == 0); first by rewrite (eqP p0) div0p mu0 sub0n. case: (@mu_spec p x); rewrite ?p0 // => q hq hp. rewrite {1}hp -{1}(subnK hn) exprD mulrA. rewrite Pdiv.IdomainMonic.mulpK; last by apply: monic_exp; apply: monicXsubC. rewrite mu_mul ?mulf_eq0 ?expf_eq0 ?polyXsubC_eq0 ?andbF ?orbF; last first. by apply: contra hq; move/eqP->; rewrite root0. by rewrite mu_exp muNroot // add0n mu_XsubC mul1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)