proposition: Lemma tallyK s : perm_eq (tally_seq (tally s)) s.
proof: Proof. rewrite -[s in perm_eq _ s]cats0 -[nil]/(tseq [::]) /tally. elim: s [::] => //= x s IHs bs; rewrite {IHs}(permPl (IHs _)). rewrite perm_sym -cat1s perm_catCA {s}perm_cat2l. elim: bs => //= b bs IHbs; case: eqP => [-> | _] //=. by rewrite -cat1s perm_catCA perm_cat2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)