proposition: Theorem LRrule_langQ t1 t2 w : is_stdtab t1 -> (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=> Hstd1. split => [[u] [v] [Hcat]| [t] []]; rewrite !langQE. - move=> /eqP Ht1 /eqP Ht2. exists (RS (invstd (std (u ++ v)))); split. + apply: (LRTriple Ht1 Ht2 erefl). exact: invstd_cat_in_shsh. + by rewrite Hcat langQE. - move=> [/= p1 p2 p Ht1 <-{t2} <-{t} Hsh]. move: Hstd1; rewrite -Ht1 RSstdE => Hstd1 {Ht1 t1}. rewrite -plactic_RS => Hpl. have := Hsh; rewrite mem_shsh // => /andP[/eqP Hp1 /eqP Hp2]. have Hszp1: size p1 <= size w. move/size_plact: Hpl; rewrite size_invstd size_std => ->. by rewrite -Hp1 size_filter count_size. have HgtnE : (fun x => (x < size p1)%O) =1 gtn (size p1). by move=> x /=; rewrite ltEnat. have HleqE : (fun x => (x >= size p1)%O) =1 leq (size p1). by move=> x /=; rewrite leEnat. exists (take (size p1) w), (drop (size p1) w); split. + by rewrite cat_take_drop. + rewrite langQE -plactic_RS -sfiltergtn_invstd // -{2}Hp1. rewrite /sfiltergtn /= -!(eq_filter HgtnE). exact: plactic_filter_gt. + rewrite langQE -plactic_RS -sfilterleq_invstd // -{1}Hp2. rewrite /sfilterleq /= -!(eq_filter HleqE). apply: plact_map_in_incr; last exact: plactic_filter_le. move=> /= x y. rewrite !mem_filter !leEnat !ltEnat /= => /andP[Hx _] /andP[Hy _] Hxy. by rewrite -(ltn_add2r (size p1)) ?subnK. 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