proposition: Lemma plact_uniq_rev u v : uniq u -> u =Pl v -> rev u =Pl rev v.
proof: Proof. Proof using. move=> Huniq. have {}Huniq x y z : rev u =Pl rev (x ++ y ++ z) -> uniq y. move=> Hpl; have : uniq (x ++ y ++ z). rewrite -rev_uniq -(perm_uniq (s1 := rev u)) ?rev_uniq //. exact: plact_homog. by rewrite !cat_uniq => /and4P[_ _]. move: v; apply: gencongr_ind => [| x y1 z y2 Hv /plactruleP[]] /=; first exact: plact_refl. - move/plact1P => [a] [b] [c] [/andP[Hab Hbc] Hy1 Hy2]. apply (plact_trans Hv); rewrite !rev_cat -!catA; apply: plact_is_congr. rewrite Hy1 Hy2 /rev /=; apply rule_gencongr. apply/plactruleP/or4P => /=. move: Hv => /Huniq; rewrite Hy1 /= => /andP[]. rewrite mem_seq2 negb_or => /andP[_ Hanb] _. by rewrite !lt_neqAle Hab Hanb (ltW Hbc) /= !mem_seq1 eq_refl ?orbT. - move/plact1iP => [a] [b] [c] [/andP[Hab Hbc] Hy2 Hy1]. apply (plact_trans Hv); rewrite !rev_cat -!catA; apply: plact_is_congr. rewrite Hy1 Hy2 /rev /=; apply rule_gencongr. apply/plactruleP/or4P => /=. move: Hv => /Huniq; rewrite Hy1 /= => /and3P[] _. rewrite mem_seq1 => Hanb _. by rewrite !lt_neqAle Hab Hanb (ltW Hbc) /= !mem_seq1 eq_refl ?orbT. - move/plact2P => [a] [b] [c] [/andP[Hab Hbc] Hy1 Hy2]. apply (plact_trans Hv); rewrite !rev_cat -!catA; apply: plact_is_congr. rewrite Hy1 Hy2 /rev /=; apply rule_gencongr. apply/plactruleP/or4P => /=. move: Hv => /Huniq; rewrite Hy1 /= => /andP[]. rewrite mem_seq2 negb_or => /andP[_ Hbnc] _. by rewrite !lt_neqAle Hbc Hbnc (ltW Hab) /= !mem_seq1 eq_refl ?orbT. - move/plact2iP => [a] [b] [c] [/andP[Hab Hbc] Hy2 Hy1]. apply (plact_trans Hv); rewrite !rev_cat -!catA; apply: plact_is_congr. rewrite Hy1 Hy2 /rev /=; apply rule_gencongr. apply/plactruleP/or4P => /=. move: Hv => /Huniq; rewrite Hy1 /= => /and3P[]. rewrite mem_seq2 negb_or => /andP[Hbnc _] _ _. by rewrite !lt_neqAle Hbc Hbnc (ltW Hab) /= !mem_seq1 eq_refl ?orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr