proposition: Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s].
proof: Proof. have /andP[Ubs _] := tallyP s; pose b := [fun s x => (x, count_mem x (tseq s))]. suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))). congr perm_eq: (perm_map (b (tally s)) (tallyEl s)). by under eq_map do rewrite /= (permP (tallyK s)). elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}]. rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n. rewrite (count_memPn _) ?addn0 ?perm_cons; last first. apply: contra bs'x; elim: {b IHbs}bs => //= b bs IHbs. by rewrite mem_cat mem_nseq inE andbC; case: (_ == _). congr perm_eq: IHbs; apply/eq_in_map=> y bs_y; congr (y, _). by rewrite count_cat count_nseq /= (negPf (memPnC bs'x y bs_y)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)