proposition: Lemma mu_opp p x : \mu_x (-p) = \mu_x p.
proof: Proof. rewrite -mulN1r -polyC1 -polyCN mul_polyC mu_mulC //. by rewrite -oppr0 (inj_eq (inv_inj (@opprK _))) oner_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)