proposition: Theorem pred_LRtriple_conj t1 t2 t : is_stdtab t1 -> is_stdtab t2 -> is_stdtab t -> pred_LRtriple t1 t2 t = pred_LRtriple (conj_tab t1) (conj_tab t2) (conj_tab t).
proof: Proof. Proof using . move=> Ht1 Ht2 Ht. have Hc1 := is_stdtab_conj Ht1. have Hc2 := is_stdtab_conj Ht2. have Hc := is_stdtab_conj Ht. apply/idP/idP => /LRtripleP H; apply/LRtripleP => //=. - apply: LRtriple_conj => //; exact: H. - rewrite -[t1]conj_tabK; last by move: Ht1 => /andP[]. rewrite -[t2]conj_tabK; last by move: Ht2 => /andP[]. rewrite -[t]conj_tabK; last by move: Ht => /andP[]. apply: LRtriple_conj => //; exact: H. 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