proposition: Lemma perm_tally s1 s2 : perm_eq s1 s2 -> perm_eq (tally s1) (tally s2).
proof: Proof. move=> eq_s12; apply: (@perm_trans _ [seq (x, count_mem x s2) | x <- undup s1]). by congr perm_eq: (tallyE s1); under eq_map do rewrite (permP eq_s12). by rewrite (permPr (tallyE s2)); apply/perm_map/perm_undup/(perm_mem eq_s12). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)