proposition: Corollary RStabmap_std (d : unit) (T : inhOrderType d) (w : seq T) : (RStabmap (std w)).2 = (RStabmap w).2.
proof: Proof. rewrite /RStabmap. move H : (RSmap w) => [P Q]. move Hs : (RSmap (std w)) => [Ps Qs] /=. by rewrite -[Q]/(P, Q).2 -H -[Qs]/(Ps, Qs).2 -Hs RSmap_std. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv