proposition: Lemma plact_col u v : sorted >%O u -> u =Pl v -> u = v.
proof: Proof. Proof using. move=> Hcolu; move: v; apply: gencongr_ind => [// |] x y1 z y2 Hu /plactruleP[]. - move/plact1P => [a] [b] [c] [/andP[Hab Hbc] Hy _]; exfalso. move: Hcolu; rewrite Hu Hy => /sorted_center /= /and3P[]. by rewrite ltNge (le_trans Hab (ltW Hbc)). - move/plact1iP => [a] [b] [c] [/andP[Hab Hbc] _ Hy]; exfalso. move: Hcolu; rewrite Hu Hy => /sorted_center /= /and3P[_]. by rewrite ltNge Hab. - move/plact2P => [a] [b] [c] [/andP[Hab Hbc] Hy _]; exfalso. move: Hcolu; rewrite Hu Hy => /sorted_center /= /and3P[_]. by rewrite ltNge (le_trans (ltW Hab) Hbc). - move/plact2iP => [a] [b] [c] [/andP[Hab Hbc] _ Hy]; exfalso. move: Hcolu; rewrite Hu Hy => /sorted_center /= /and3P[]. by rewrite ltNge Hbc. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr