proposition: Lemma bump_size_ins : bump -> size ins = size Row.
proof: Proof. Proof using HRow. move/bump_inspos_lt_size; rewrite /insE /insmin size_set_nth maxnC /maxn leqNgt. by move/negbTE => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab