proposition: Lemma mu_polyC c x : \mu_x (c%:P) = 0%N.
proof: Proof. case c0: (c == 0); first by rewrite (eqP c0) mu0. by apply: muNroot; rewrite rootC c0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)