proposition: Corollary RSinvstdE (disp : unit) (T : inhOrderType disp) (w : seq T) : RS (invstd (std w)) = (RStabmap w).2.
proof: Proof. rewrite -RStabmapE RSTabmapstdE /RStabmap. rewrite [LHS](_ : _ = stdtab_of_yam (RSmap (std w)).2); last by case: RSmap. rewrite [RHS](_ : _ = stdtab_of_yam (RSmap w).2); last by case: RSmap. by congr (stdtab_of_yam _); exact: 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