proposition: Lemma size_count_mem_undup (s : seq T) : size s = \sum_(j <- undup s) count_mem j s.
proof: Proof. Proof using. have -> : size s = \sum_(i <- s) 1. by elim: s => [|s0 s /= ->] /=; rewrite ?big_nil // big_cons add1n. rewrite -big_undup_iterop_count /=; apply eq_bigr => i _. rewrite Monoid.iteropE /=. by elim: (count_mem i s) => {i} //= i ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles