proposition: Lemma sfilterleq_LRsupport_skew Q : Q \in LRtab_set P1 P2 P -> is_skew_reshape_tableau P P1 (sfilterleq d1 (to_word Q)).
proof: Proof. Proof using Hincl. have:= stdtabnP (hyper_stdtabn P2); rewrite /is_stdtab => /andP[Htab2 Hstd2]. have /allP /= Hall := RSclassP Htab2. move=> HLRtab. have := HLRtab; rewrite /LRtab_set inE => /andP[HLR /eqP Hshape]. have Hfilter := filtergtn_LRsupport HLR. have:= HLR; rewrite inE /= => /hasP[p2 {}/Hall /Sch_plact Hpl Hshsh]. have:= hyper_stdtabnP P1 => /=. rewrite /is_stdtab => /andP[/andP[_ Hstd] /= /eqP Hsz]. have:= (shsh_sfilterleq Hstd Hshsh). rewrite size_to_word {Hstd}Hsz /= => Hp2; subst p2. apply (eq_inv_is_skew_tableau_reshape (u1 := [seq x <- to_word Q | d1 <= x])). - exact: size_included. - apply/eq_invP; split; first by rewrite size_map. move=> i j /andP[Hij Hj]. rewrite (nth_map inh); last exact: (leq_ltn_trans Hij Hj). rewrite (nth_map inh); last exact: Hj. rewrite !leEnat leq_subLR subnKC //=. by have:= mem_nth inh Hj; rewrite mem_filter => /andP[]. - move: Hpl => /plact_homog/perm_size. rewrite size_map => ->. by rewrite size_std sumn_diff_shape_intpartE -evalseq_eq_size evalseq_hyper_yam. - rewrite (filterleq_LRsupport HLRtab). have -> : val P1 = shape (filter_gt_tab d1 Q). by rewrite Hfilter -{1}(shaped_hyper_stdtabnP P1) /=. apply is_skew_tableau_filter_le; 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