proposition: Lemma mu_add p q x : p + q != 0 -> (minn (\mu_x p) (\mu_x q) <= \mu_x (p + q)%R)%N .
proof: Proof. have [->|p0] := eqVneq p 0; first by rewrite mu0 min0n add0r. have [->|q0] := eqVneq q 0; first by rewrite mu0 minn0 addr0. have [Hpq|Hpq|Hpq] := (ltngtP (\mu_x p) (\mu_x q)). + by rewrite mu_addr ?geq_minl. + by rewrite mu_addl ?geq_minr. have [//|p' nrp'x hp] := (@mu_spec _ p x). have [//|q' nrq'x hq] := (@mu_spec _ q x). rewrite Hpq hp {1 3}hq Hpq -mulrDl => pq0. by rewrite mu_mul // mu_exp mu_XsubC mul1n leq_addl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)