proposition: Lemma bijLR_surj Q : Q \in LRtab_set P1 P2 P -> exists2 yam, yam \in LRyam_set & bijLR yam = Q.
proof: Proof. Proof using . move=> HLRtab; have:= HLRtab; rewrite /LRtab_set inE => /andP[HLR /eqP Hshape]. have:= HLR => /sfilterleq_LRsupportP[] y Hmap. have Hskew : is_skew_reshape_tableau P P1 y. rewrite /is_skew_reshape_tableau (is_skew_tableau_reshape_std (size_included Hincl)). + rewrite Hmap; exact: sfilterleq_LRsupport_skew. + by rewrite size_yameval sumn_diff_shape_intpartE. exists y. - rewrite inE /=; exact Hskew. - rewrite /bijLR. case (boolP (is_skew_reshape_tableau P P1 y)) => /=; last by rewrite Hskew. move=> pf; apply val_inj => /= {pf}. have -> : hyper_stdtab P1 = filter_gt_tab d1 Q. have:= hyper_stdtabnP P1 => /andP[Htab1 /eqP Hsz1]. rewrite inE in HLR. rewrite (pred_LRtriple_fast_filter_gt Htab1 (stdtabnP Q) HLR). by rewrite Hsz1. have -> : [seq shiftn d1 i | i <- skew_reshape P1 P (std y)] = filter_le_tab d1 Q. rewrite Hmap /= /skew_reshape map_rev map_reshape -/(shiftn d1) sfilterleqK. by rewrite -/(skew_reshape _ _ _) filterleq_LRsupport. rewrite join_tab_filter //=; exact: stdtabP. 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