proposition: Lemma mu_addl p q x : q != 0 -> (\mu_x p > \mu_x q)%N -> \mu_x (p + q) = \mu_x q.
proof: Proof. by move=> q0 hmu; rewrite addrC mu_addr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)