proposition: Lemma nbump_inspos_eq_size : ~~bump -> pos = size Row.
proof: Proof. Proof using HRow. by move=> Hnbump; rewrite -insposE nbump_mininspredE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab