proposition: Lemma pred_LRtriple_fast_bijLRyam (yam : yameval P2) : is_skew_reshape_tableau P P1 yam -> pred_LRtriple_fast (hyper_stdtabn P1) (hyper_stdtabn P2) (bijLRyam yam).
proof: Proof. Proof using Hincl. rewrite/is_skew_reshape_tableau => Hskew. apply/hasP; exists (std yam). rewrite RSclassE; last exact: is_tableau_RS. rewrite -plactic_RS. apply: std_plact. have /= <- := eval_yameval yam. apply yam_plactic_hyper; exact: yamevalP. have Hstd1 : is_std (to_word (hyper_stdtabn P1)). have /= := hyper_stdtabnP P1 => /andP[]. by rewrite /is_stdtab => /andP[]. rewrite -[std yam](to_word_skew_reshape Hincl); first last. by rewrite size_std size_yameval sumn_diff_shape_intpartE. rewrite /= -{2}(size_tab_stdtabn (hyper_stdtabn P1)). apply: join_stdtab_in_shuffle. - rewrite RSstdE; exact: std_is_std. - exact: size_leq_skew_reshape. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur