proposition: Lemma is_stdtab_of_n_LRtriple t1 t2 t : is_stdtab t1 -> is_stdtab t2 -> LRtriple t1 t2 t -> is_stdtab_of_n ((size_tab t1) + (size_tab t2)) t.
proof: Proof. Proof using . move=> H1 H2 [p1 p2 p Hp1 Hp2 <- {t} Hp] /=. apply/andP; split. - rewrite RSstdE. have Hsp1 : is_std p1 by rewrite -(RSstdE) Hp1. have Hsp2 : is_std p2 by rewrite -(RSstdE) Hp2. exact: (allP (std_shsh Hsp1 Hsp2)). - rewrite size_RS; move: Hp; rewrite /shsh => Hp. have /allP/(_ _ Hp)/eqP -> := all_size_shuffle p1 (shiftn (size p1) p2). by rewrite size_map -Hp1 -Hp2 !size_RS. 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