proposition: Lemma mu_eq0 : forall p x, p != 0 -> (\mu_x p == 0%N) = (~~ root p x).
proof: Proof. by move=> p x p0; rewrite -mu_gt0 // -leqNgt leqn0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)