proposition: Lemma pred_LRtriple_fast_filter_gt t1 t2 t : is_stdtab t1 -> is_stdtab t -> pred_LRtriple_fast t1 t2 t -> t1 = filter_gt_tab (size_tab t1) t.
proof: Proof. Proof using . move=> Ht1 Ht /= /hasP[p2 Hp2 Hshsh]. move: Ht1; rewrite /is_stdtab => /andP[Htab1 Hstd1]. rewrite -{1}(RS_tabE Htab1) (shsh_sfiltergtn Hstd1 Hshsh) /=. rewrite -size_to_word. move: Ht; rewrite /is_stdtab => /andP[Htab _]. by rewrite filter_gt_RS /= (RS_tabE Htab). 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