proposition: Lemma muP p x n : p != 0 -> (('X - x%:P)^+n %| p) && ~~(('X - x%:P)^+n.+1 %| p) = (n == \mu_x p).
proof: Proof. by move=> hp0; rewrite !root_le_mu//; case: (ltngtP n (\mu_x p)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)