proposition: Lemma bijLRyamP (yam : yameval P2) : is_skew_reshape_tableau P P1 yam -> is_stdtab_of_n (d1 + d2) (bijLRyam yam).
proof: Proof. Proof using Hincl. rewrite /is_skew_reshape_tableau /= /is_stdtab => Hskew. rewrite (_ : size_tab _ = d1 + d2); first last. rewrite size_join_tab. + rewrite size_RS size_std size_hyper_yam sumn_intpartn; congr (_ + _). rewrite /size_tab /shape -map_comp. rewrite (eq_map (g := size)); last by move=> s /=; rewrite size_map. rewrite -/(shape _) (shape_skew_reshape Hincl). * by rewrite (sumn_diff_shape Hincl) !sumn_intpartn addKn. * by rewrite size_std size_yameval sumn_diff_shape_intpartE. + rewrite size_map; exact: size_leq_skew_reshape. rewrite eq_refl andbT. apply/andP; split. - rewrite -{2}(size_tab_stdtabn (hyper_stdtabn P1)). apply join_stdtab. rewrite RSstdE; exact: std_is_std. - rewrite shape_RS_std shape_RS_yam; last by apply hyper_yamP; apply intpartnP. rewrite (evalseq_hyper_yam (intpartnP P1)). rewrite -(is_skew_tableau_reshape_std (size_included Hincl)). + exact: Hskew. + by rewrite size_yameval sumn_diff_shape_intpartE. - have /= /hasP[] := pred_LRtriple_fast_bijLRyam Hskew => z. move: (to_word _) => image. rewrite (RSclassE _ (is_tableau_RS _)) -plactic_RS => /plact_homog Hz. have {}Hz : is_std z by apply: (perm_std _ Hz); apply std_is_std. have : is_stdtab (RS (std (hyper_yam P1))) by rewrite RSstdE; apply std_is_std. rewrite /is_stdtab => /andP[_ Hstd1]. exact: (allP (std_shsh Hstd1 Hz)). 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