proposition: Lemma sfilterleq_LRsupportP Q : Q \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2) -> exists y : yameval P2, std y = (sfilterleq d1 (to_word Q)).
proof: Proof. Proof using . rewrite /LRsupport inE -LRtriple_fastE //. move/(LRtripleP _ (stdtabnP (hyper_stdtabn P1)) (stdtabnP (hyper_stdtabn P2))). move=> [p1 p2 p]; rewrite /hyper_stdtab => Hp1 Hp2 Hp. have Hstdp1 : is_std p1 by rewrite -RSstdE Hp1. rewrite (mem_shsh _ _ Hstdp1) => /andP[]. rewrite -(size_RS p1) Hp1. rewrite (size_tab_stdtabn (hyper_stdtabn P1)) => /eqP Hsfp1 /eqP Hsfp2. suff : sfilterleq d1 (to_word Q) =Pl std (hyper_yam P2). move/(plact_from_yam (intpartnP P2)) => [yam]. rewrite -[val P2]/(val (intpart_of_intpartn P2)) => Hyam. by exists (YamEval Hyam). rewrite /=/hyper_stdtab in Hp2. rewrite -Hp plactic_RS -Hp2 -Hsfp2 eq_sym -plactic_RS. rewrite /sfilterleq /=. apply: plact_map_in_incr. move=> i j; rewrite !mem_filter => /andP[Hi _] /andP[Hj _]. rewrite !ltEnat /= => Hij. by rewrite ltn_subRL subnKC. apply: (plactic_filter_le d1). exact: congr_RS. 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