proposition: Lemma big_mset X P F : \big[op/idx]_(i <- X | P i) F i = \big[op/idx]_(i <- finsupp X | P i) iterop (X i) op (F i) idx.
proof: Proof. rewrite [in RHS](perm_big (undup X)) 1?perm_sym ?perm_undup_mset//. rewrite -[in LHS]big_undup_iterop_count; apply: eq_bigr => i _. by rewrite count_mem_mset. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap