proposition: Lemma bump_mininspredE (Hbump : bump) : mininspred = ex_minn (ex_intro inspred (size Row).-1 (transf Hbump)).
proof: Proof. Proof using. rewrite /mininspred /inspred; apply/eqP. case (ltP l (last l Row)) => Hlast. - case (ex_minnP (ex_intro _ _ _)) => pos1 Hl1 Hpos1. case (ex_minnP (ex_intro _ _ _)) => pos2 Hl2 Hpos2. by rewrite eqn_leq (Hpos1 _ Hl2) (Hpos2 _ Hl1). - by exfalso; move: Hbump; rewrite /bump /= ltNge Hlast. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab