proposition: Lemma RStabE (w : seq T) : (RStab w).1 = (RS w).
proof: Proof. Proof using . by rewrite RStabmapE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly