proposition: Lemma RSmapE w : (RSmap w).1 = RS w.
proof: Proof. Proof using. elim/last_ind: w => [| w wn] //=; rewrite /RSmap /RS rev_rcons /= -instabnrowE. case: (RSmap_rev (rev w)) => [t rows] /= ->. by case: (instabnrow (RS_rev (rev w)) wn). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab