proposition: Theorem LRtriple_cat_equiv t1 t2 : is_stdtab t1 -> is_stdtab t2 -> forall u1 u2 : word, ( (u1 \in langQ t1 /\ u2 \in langQ t2) <-> [/\ size u1 = size_tab t1, size u2 = size_tab t2 & exists t, LRtriple t1 t2 t /\ u1 ++ u2 \in langQ t] ).
proof: Proof. Proof using . move=> Hstd1 Hstd2 u1 u2. split. - move=> [Hu1 Hu2]; split; try exact: size_langQ. exists (RStabmap (u1 ++ u2)).2; split. + exact: LRtriple_cat_langQ. + by rewrite inE. - move=> [Hsz1 Hsz2 [t] [] [p1 p2 p Hp1 Hp2 Htmp]]; subst t. rewrite !inE -!RSinvstdE -Hp1 -Hp2 -!plactic_RS => Hsh Hcat. have Hstdp1 : is_std p1 by rewrite -RSstdE Hp1. have Hszp : size p1 = size u1 by rewrite Hsz1 -size_RS Hp1. split. + rewrite (invstd_catgtn u1 u2) (shsh_sfiltergtn Hstdp1 Hsh) Hszp. exact: plactic_filter_gt. + rewrite (invstd_catleq u1 u2) (shsh_sfilterleq Hstdp1 Hsh) Hszp. rewrite (shift_plactcongr (size u1)) !sfilterleqK. exact: plactic_filter_le. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype finfun fintype choice) mathcomp(order seq tuple finset perm binomial bigop) tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab Schensted plactic Greene_inv stdplact