proposition: Corollary RSTabmapstdE (disp : unit) (T : inhOrderType disp) (w : seq T) : (RStabmap (invstd (std w))).1 = (RStabmap (std w)).2.
proof: Proof. have := invstdRSE (std_is_std w). by case (RStabmap (invstd (std w))) => [P Q] /= ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv