proposition: Corollary invstdRSE s : is_std s -> let (P, Q) := RStabmap (invstd s) in RStabmap s = (Q, P).
proof: Proof. move=> Hstd. case H : (RStabmap (invstd s)) => [P Q]. by rewrite (invseqRSE (invseq_invstd Hstd)) H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv