proposition: Lemma mu_mulC c p x : c != 0 -> \mu_x (c *: p) = \mu_x p.
proof: Proof. move=> cn0; case p0: (p == 0); first by rewrite (eqP p0) scaler0. by rewrite -mul_polyC mu_mul ?mu_polyC// mulf_neq0 ?p0 ?polyC_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)