proposition: Corollary invseqRSE s t : invseq s t -> RStabmap s = ((RStabmap t).2, (RStabmap t).1).
proof: Proof. move=> Hinv. rewrite -(invseqRSPQE Hinv) (invseqRSPQE (invseq_sym Hinv)). by case (RStabmap s). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv