proposition: Lemma plact_ltrans : left_transitive plactcongr.
proof: Proof. Proof using. by have:= plact_equiv; rewrite equivalence_relP => [] [Hrefl Hltr]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr