proposition: Lemma mu_mul p q x : p * q != 0 -> \mu_x (p * q) = (\mu_x p + \mu_x q)%N.
proof: Proof. move=> hpqn0; apply/eqP; rewrite eq_sym -muP//. rewrite exprD dvdp_mul ?root_mu//=. move: hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0. move: (mu_spec x hp0)=> [qp qp0 hp]. move: (mu_spec x hq0)=> [qq qq0 hq]. rewrite {2}hp {2}hq exprS exprD !mulrA [qp * _ * _]mulrAC. rewrite !dvdp_mul2r ?expf_neq0 ?polyXsubC_eq0 // -eqp_div_XsubC. move: (mulf_neq0 qp0 qq0); rewrite -hornerM; apply: contra; move/eqP->. by rewrite hornerM hornerXsubC subrr mulr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)