proposition: Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).
proof: Proof. have /andP[Ubs bs'0] := tallyP s; set bs := tally s in Ubs bs'0 *. rewrite uniq_perm ?undup_uniq {Ubs}// => x. rewrite mem_undup -(perm_mem (tallyK s)) -/bs. elim: bs => [|[y [|m]] bs IHbs] //= in bs'0 *. by rewrite inE IHbs // mem_cat mem_nseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)