proposition: Lemma bump_inspos_lt_size : bump -> pos < size Row.
proof: Proof. Proof using HRow. rewrite -insposE /bump; move=> Hbump; rewrite (bump_mininspredE Hbump). case (ex_minnP (ex_intro _ _ _)) => pos _ /(_ _ (transf Hbump)). case: Row Hbump; first by rewrite /= ltxx. by move=> l0 r _ /=; rewrite ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab