proposition: Lemma muNroot p x : ~~ root p x -> \mu_x p = 0%N.
proof: Proof. case p0: (p == 0); first by rewrite (eqP p0) rootC eqxx. by move=> pnx0; apply/eqP; rewrite -leqn0 leqNgt mu_gt0 ?p0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)