proposition: Lemma mu_XsubC x : \mu_x ('X - x%:P) = 1%N.
proof: Proof. apply/eqP; rewrite eq_sym -muP; last by rewrite polyXsubC_eq0. by rewrite expr1 dvdpp/= -{2}[_ - _]expr1 dvdp_Pexp2l // size_XsubC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(ssralg poly ssrnum zmodp polydiv interval)