proposition: Theorem LRrule_langQ_alternate t1 t2 w : is_stdtab t1 -> is_stdtab t2 -> (exists u v, [/\ w = u ++ v, u \in langQ t1 & v \in langQ t2]) <-> (exists t, LRtriple t1 t2 t /\ w \in langQ t).
proof: Proof. move=> H1 H2; have H := LRtriple_cat_equiv H1 H2. split=> [[u] [v] [Hcat Hu Hv]| [t] [Htriple Hw]]. - have {}/H [_ _] : u \in langQ t1 /\ v \in langQ t2 by split. by rewrite Hcat. - have:= cat_take_drop (size_tab t1) w. set u1 := take (size_tab t1) w; set u2 := drop (size_tab t1) w => Hcat. have /= /andP[_ /eqP Hsz] := is_stdtab_of_n_LRtriple H1 H2 Htriple. have Hszw : size w = size_tab t. move: Hw; rewrite langQE => /eqP <-. by rewrite size_RS size_invstd size_std. have : [/\ size u1 = size_tab t1, size u2 = size_tab t2 & exists t : seq (seq nat), LRtriple t1 t2 t /\ u1 ++ u2 \in langQ t]. split. - by rewrite size_takel // Hszw Hsz leq_addr. - by rewrite size_drop Hszw Hsz addnC addnK. - by exists t; rewrite Hcat. rewrite -H => [] [Hu1 Hu2]. by exists u1, u2; rewrite Hcat. 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