proposition: Theorem LRtriple_cat_langQ t1 t2 u1 u2: is_stdtab t1 -> is_stdtab t2 -> u1 \in langQ t1 -> u2 \in langQ t2 -> LRtriple t1 t2 (RStabmap (u1 ++ u2)).2.
proof: Proof. Proof using . move=> Hstd1 Hstd2 Hu1 Hu2. have Hsz1 := size_langQ Hu1; have Hsz2 := size_langQ Hu2. move: Hu1 Hu2; rewrite !inE => /eqP Hu1 /eqP Hu2. apply: (LRTriple (p1 := invstd (std u1)) (p2 := invstd (std u2)) (p := invstd (std (u1 ++ u2))) ). - by rewrite -Hu1 RSinvstdE. - by rewrite -Hu2 RSinvstdE. - by rewrite RSinvstdE. - exact: invstd_cat_in_shsh. 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