proposition: Lemma coef_sumMXn I (r : seq I) (P : pred I) (p : I -> R) (n : I -> nat) k : (\sum_(i <- r | P i) p i *: 'X^(n i))`_k = \sum_(i <- r | P i && (n i == k)) p i.
proof: Proof. rewrite coef_sum big_mkcondr; apply: eq_bigr => i Pi. by rewrite coefZ coefXn mulr_natr mulrb eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)