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