proposition: Lemma toDepRSPair (u : seq T) d (t : stdtabn d) : forall H : is_RStabpair (RS u, val t), RSmapinv2 (RS u, yam_of_stdtab t) = RStabinv (RSTabPair H).
proof: Proof. Proof using . by []. 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