proposition: Lemma bump_insposE : bump -> mininspred = pos.
proof: Proof. Proof using. move=> Hbump; rewrite (bump_mininspredE Hbump). case: (ex_minnP (ex_intro _ _ _)) => pos Hl Hpos. move/(_ _ (inspred_inspos Hbump)): Hpos => Hleq. case (ltnP pos (inspos Row l)) => H2. - by exfalso; move: Hl; rewrite (negbTE (inspredN_lt_inspos H2)). - by apply/eqP; rewrite eqn_leq Hleq H2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab