proposition: Corollary Sch_plact u v : RS u == RS v -> u =Pl v .
proof: Proof. Proof using. move=> /eqP Heq. apply: (@plact_trans _ _ (to_word (RS u))); first exact: congr_RS. by rewrite Heq plact_sym; exact: congr_RS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr