proposition: Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs).
proof: Proof. by rewrite size_flatten /shape -map_comp; under eq_map do rewrite /= size_nseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)