proposition: Lemma root_le_mu p x n : p != 0 -> ('X - x%:P)^+n %| p = (n <= \mu_x p)%N.
proof: Proof. move=> pn0; case: leqP=> hn; last apply/negP=> hp. apply: (@dvdp_trans _ (('X - x%:P) ^+ (\mu_x p))); last by rewrite root_mu. by rewrite dvdp_Pexp2l // size_XsubC. suff : ('X - x%:P) ^+ (\mu_x p).+1 %| p by rewrite root_muN. by apply: dvdp_trans hp; rewrite dvdp_Pexp2l // size_XsubC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)