proposition: Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F : \big[*%M/1]_(i <- undup r | P i) iterop (count_mem i r) *%M (F i) 1 = \big[*%M/1]_(i <- r | P i) F i.
proof: Proof. rewrite -[RHS](perm_big _ F (perm_count_undup _)) big_flatten big_map. by rewrite [LHS]big_mkcond; apply: eq_bigr=> i _; rewrite big_nseq_cond iteropE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)