proposition: Lemma size_plact u v : plactcongr u v -> size u = size v.
proof: Proof. Proof using. by move/plact_homog/perm_size. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr