proposition: Lemma sum_mset (X : {mset K}) (P : pred K) (F : K -> nat) : \sum_(i <- X | P i) F i = \sum_(i <- finsupp X | P i) X i * F i.
proof: Proof. rewrite big_mset; apply: eq_bigr => i _ //. by rewrite Monoid.iteropE iter_addn addn0 mulnC. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap