proposition: Lemma perm_count_undup s : perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.
proof: Proof. by rewrite -(permPr (tallyK s)) (permPr (perm_tseq (tallyE s))) /tseq -map_comp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)