proposition: Lemma inspos_leq_exP i : inspred i -> pos <= i.
proof: Proof. Proof using HRow. move=> HlPred. rewrite -insposE (bump_mininspredE (inspred_any_bump HlPred)). case (ex_minnP (ex_intro _ _ _)) => pos _ Hpos. exact: Hpos. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab