proposition: Lemma instabnrowE t l : (instabnrow t l).1 = instab t l.
proof: Proof. Proof using. elim: t l => [// | t0 t IHt] l /=. case (bumprow t0 l) => [[ll | //] rr]. by move/(_ ll): IHt; case (instabnrow t ll) => [tres nres] /= ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab