proposition: Lemma tallyP s : tally s \is a wf_tally.
proof: Proof. rewrite /tally; set bs := [::]; have: bs \in wf_tally by []. by elim: s bs => //= x s IHs bs /(incr_tallyP x)/IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)