proposition: Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}.
proof: Proof. move=> bs /andP[]; elim: bs => [|[x [|n]] bs IHbs] //= /andP[bs'x Ubs] bs'0. rewrite inE /tseq /tally /= -[n.+1]addn1 in bs'0 *. elim: n 1 => /= [|n IHn] m; last by rewrite eqxx IHn addnS. rewrite -{}[in RHS]IHbs {Ubs bs'0}// /tally /tally_seq add0n. elim: bs bs'x [::] => [|[y n] bs IHbs] //= /[1!inE] /norP[y'x bs'x]. by elim: n => [|n IHn] bs1 /=; [rewrite IHbs | rewrite eq_sym ifN // IHn]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)