proposition: Lemma mu_gt0 p x : p != 0 -> (0 < \mu_x p)%N = root p x.
proof: Proof. by move=> pn0; rewrite -root_le_mu// expr1 root_factor_theorem. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)