proposition: Lemma inspred_inspos : bump -> inspred pos.
proof: Proof. Proof using. rewrite /inspred /bump; elim: Row => [// | l0 [_ /= H | l1 r /= IHr]]. - by rewrite H /= H. - by move/IHr; case: (ltP l l0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab