proposition: Lemma plact_sym : symmetric plactcongr.
proof: Proof. Proof using. have:= plact_equiv; rewrite equivalence_relP => [] [Hrefl Hltr]. by move=> i j; apply/idP/idP => /Hltr <-. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr