proposition: Lemma mu_addr p q x : p != 0 -> (\mu_x p < \mu_x q)%N -> \mu_x (p + q) = \mu_x p.
proof: Proof. move=> pn0 mupq. have pqn0 : p + q != 0. move: mupq; rewrite ltnNge; apply: contra. by rewrite -[q]opprK subr_eq0; move/eqP->; rewrite opprK mu_opp leqnn. have qn0: q != 0 by move: mupq; apply: contraL; move/eqP->; rewrite mu0 ltn0. case: (mu_spec x pn0)=> [qqp qqp0] hp. case: (mu_spec x qn0)=> [qqq qqq0] hq. rewrite hp hq -(subnK (ltnW mupq)). rewrite mu_mul ?mulf_eq0; last first. rewrite expf_eq0 polyXsubC_eq0 andbF orbF. by apply: contra qqp0; move/eqP->; rewrite root0. rewrite mu_exp mu_XsubC mul1n [\mu_x qqp]muNroot // add0n. rewrite exprD mulrA -mulrDl mu_mul; last first. by rewrite mulrDl -mulrA -exprD subnK 1?ltnW // -hp -hq. rewrite muNroot ?add0n ?mu_exp ?mu_XsubC ?mul1n //. rewrite rootE !hornerE ?horner_exp ?hornerXsubC subrr. by rewrite -subnSK // subnS exprS mul0r mulr0 addr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)