proposition: Lemma size_invins b s : size (invins b s) = (size s).
proof: Proof. Proof using. rewrite /invins; elim: s => [// | s0 s] /=. case H : (invbumprow b s) => [r a] /=. by case: (leP b (head b s)) => _ //= ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab