proposition: Lemma LRtab_set_included (P : 'P_(d1 + d2)) Q : Q \in LRtab_set P1 P2 P -> included P1 P.
proof: Proof. Proof using . rewrite !inE => /andP[Hhas /eqP <-]. rewrite -(shaped_hyper_stdtabnP P1) /=. have : pred_LRtriple_fast (hyper_stdtabn P1) (hyper_stdtabn P2) Q by []. move/(pred_LRtriple_fast_filter_gt (stdtabnP (hyper_stdtabn P1)) (stdtabnP Q))=> /= ->. case: Q {Hhas} => Q /= /andP[]. rewrite /is_stdtab => /andP[HQ _] _. exact: included_shape_filter_gt_tab. 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