proposition: Lemma root_muN p x : p != 0 -> (('X - x%:P)^+(\mu_x p).+1 %| p) = false.
proof: Proof. move=> pn0; case: (mu_spec x pn0)=> q qn0 hp /=. rewrite {2}hp exprS dvdp_mul2r; last first. by rewrite expf_neq0 // polyXsubC_eq0. apply: negbTE; rewrite -eqp_div_XsubC; apply: contra qn0. by move/eqP->; rewrite rootM root_XsubC eqxx orbT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)