proposition: Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}.
proof: Proof. move=> bs /andP[]; rewrite unfold_in. elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs] /[1!inE] /= bs'0. have [<- | y'x] /= := eqVneq y; first by rewrite bs'y Ubs. rewrite -andbA {}IHbs {Ubs bs'0}// andbT. elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y]. by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)