proposition: Lemma plact_row u v : is_row u -> u =Pl v -> u = v.
proof: Proof. Proof using. move=> Hrowu; move: v; apply: gencongr_ind => [// |] x y1 z y2 Hu /plactruleP[]. - move/plact1P => [a] [b] [c] [/andP[Hab Hbc] Hy _]; exfalso. move: Hrowu; rewrite Hu Hy => /is_row_cat2[_]/is_row_cat2[] /= /and3P[_]. by rewrite leNgt Hbc. - move/plact1iP => [a] [b] [c] [/andP[Hab Hbc] _ Hy]; exfalso. move: Hrowu; rewrite Hu Hy => /is_row_cat2[_]/is_row_cat2[] /= /and3P[]. by rewrite leNgt (le_lt_trans Hab Hbc). - move/plact2P => [a] [b] [c] [/andP[Hab Hbc] Hy _]; exfalso. move: Hrowu; rewrite Hu Hy => /is_row_cat2[_]/is_row_cat2[] /= /and3P[]. by rewrite leNgt Hab. - move/plact2iP => [a] [b] [c] [/andP[Hab Hbc] _ Hy]; exfalso. move: Hrowu; rewrite Hu Hy => /is_row_cat2[_]/is_row_cat2[] /= /and3P[_]. by rewrite leNgt (lt_le_trans Hab Hbc). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr