proposition: Lemma LRtriple_fastE t1 t2 t : is_stdtab t1 -> is_stdtab t2 -> is_stdtab t -> pred_LRtriple t1 t2 t = pred_LRtriple_fast t1 t2 t.
proof: Proof. Proof using . move=> Ht1 Ht2 Ht. apply/idP/idP. - move/(LRtripleP t Ht1 Ht2) => [p1 p2 p Hp1 Hp2 Hp Hshsh] /=. rewrite -Hp -Hp1 -Hp2. pose p' := (sfilterleq (size p1) (to_word (RS p))). have Hp' : RS p2 = RS p'. apply/eqP; rewrite -plactic_RS. move: Hshsh; have:= Ht1; rewrite -Hp1 RSstdE => /mem_shsh -> /andP[_ /eqP <-]. rewrite (shift_plactcongr (size p1)) /p' !sfilterleqK. apply: plactic_filter_le; apply congr_RS. apply/hasP; exists p'. + apply /mapP; exists (RSmap p').2. * apply/count_memPn; rewrite Hp'. have: is_yam_of_eval (shape (RS p')) (RSmap p').2. by rewrite /is_yam_of_eval is_yam_RSmap2 /= -RSmapE shape_RSmap_eq. by move/(enum_yameval_countE (is_part_sht (is_tableau_RS p'))) => ->. * rewrite Hp' -[RS p']RSmapE /=. have -> : ((RSmap p').1, (RSmap p').2) = RSmap p' by case RSmap. by rewrite RSmapK. + have: is_std (to_word (RS p1)) by move: Ht1; rewrite Hp1 /is_stdtab => /andP[]. move/mem_shsh ->; apply/andP. rewrite size_to_word size_RS; split; last by []. move: Hshsh; have:= Ht1. rewrite -Hp1 RSstdE => /mem_shsh -> /andP[/eqP {3}<- _]. rewrite /= filter_gt_RS. by rewrite filter_to_word to_word_filter_nnil. - move=> Hfast; apply/(LRtripleP t Ht1 Ht2). move: Hfast => /= /hasP[p2 /mapP[y2 Hy2]]. have:= Ht2; rewrite /is_stdtab => /andP[Htab2 _]. have:= (is_part_sht Htab2) => /enum_yamevalP/allP/(_ _ Hy2) {Hy2}. rewrite /is_yam_of_eval => /andP[Hyam2 /eqP Hsh2] Hp2 Htshsh. have:= Ht1; rewrite /is_stdtab => /andP[/RS_tabE H1 _]. have H2 : RS p2 = t2 by rewrite Hp2 -RSmapE RSmapinv2K //= Htab2 Hyam2 Hsh2 /=. have:= Ht; rewrite /is_stdtab => /andP[/RS_tabE Hres _]. exact: (LRTriple H1 H2 Hres). 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