proposition: Lemma plact_equiv : equivalence_rel plactcongr.
proof: Proof. Proof using. by apply: gencongr_equiv; exact: plactrule_sym. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr