proposition: Lemma LRtripleP t1 t2 t : is_stdtab t1 -> is_stdtab t2 -> reflect (LRtriple t1 t2 t) (pred_LRtriple t1 t2 t).
proof: Proof. Proof using . rewrite /is_stdtab => /andP[Htab1 _] /andP[Htab2 _]. apply: (iffP idP) => /=. - move=> /hasP[p /flattenP[shuf /allpairsP[] [p1 p2]]] /= []. move=> /mapP[yam1 /(allP (enum_yamevalP (is_part_sht Htab1))) /= /andP[Hyam1 Hsh1] Hp1]. move=> /mapP[yam2 /(allP (enum_yamevalP (is_part_sht Htab2))) /= /andP[Hyam2 Hsh2] Hp2]. move=> -> {shuf} Hshuf /eqP <- {t}. apply: (@LRTriple t1 t2 (RS p) p1 p2 p) => //=. + by rewrite Hp1 -RSmapE RSmapinv2K //= Htab1 Hyam1 eq_sym Hsh1. + by rewrite Hp2 -RSmapE RSmapinv2K //= Htab2 Hyam2 eq_sym Hsh2. - move=> [p1 p2 p]; rewrite -2!RSmapE => Hp1 Hp2 Hp Hsh. apply/hasP; exists p; last by rewrite Hp. apply/flattenP; exists (shsh p1 p2); last exact: Hsh. apply/allpairsP; exists (p1, p2); split; last by []. + rewrite /= -Hp1 RSmapE; exact: mem_RSclass. + rewrite /= -Hp2 RSmapE; exact: mem_RSclass. 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