proposition: Lemma prod_mset (X : {mset K}) (P : pred K) (F : K -> nat) : \prod_(i <- X | P i) F i = \prod_(i <- finsupp X | P i) F i ^ X i.
proof: Proof. by rewrite big_mset. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap