proposition: Theorem LRtriple_conj t1 t2 t : is_stdtab t1 -> is_stdtab t2 -> is_stdtab t -> LRtriple t1 t2 t -> LRtriple (conj_tab t1) (conj_tab t2) (conj_tab t).
proof: Proof. Proof using . move=> Ht1 Ht2 Ht [p1 p2 p Hp1 Hp2 Hp]. rewrite mem_shsh; last by rewrite -RSstdE Hp1. move=> /= /andP[/eqP Hsh1 /eqP Hsh2]. apply: (@LRTriple _ _ _ (rev p1) (rev p2) (rev p)). - rewrite RS_rev_uniq; last by apply std_uniq; rewrite -RSstdE Hp1. by rewrite Hp1. - rewrite RS_rev_uniq; last by apply std_uniq; rewrite -RSstdE Hp2. by rewrite Hp2. - rewrite RS_rev_uniq; last by apply std_uniq; rewrite -RSstdE Hp. by rewrite Hp. - rewrite mem_shsh; first last. rewrite /is_std size_rev perm_rev. by rewrite -/(is_std _) -RSstdE Hp1. by rewrite /= size_rev !filter_rev map_rev Hsh1 Hsh2 !eq_refl. 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