proposition: Lemma perm_tally_seq bs1 bs2 : perm_eq bs1 bs2 -> perm_eq (tally_seq bs1) (tally_seq bs2).
proof: Proof. by move=> Ebs12; rewrite perm_flatten ?perm_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)