proposition: Lemma ins_bumprowE : insRow = bumpRow.2.
proof: Proof. Proof using. elim: Row => [// | t0 r IHr] /=. case: (ltP l t0) => _ //=. by move: IHr; case (bumprow r l) => [lr tr] /= ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab