proposition: Lemma bijLR_LRsupport yam : yam \in LRyam_set -> bijLR yam \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2).
proof: Proof. Proof using . rewrite !inE /bijLR /= => Hskew. case (boolP (is_skew_reshape_tableau P P1 yam)) => /=; last by rewrite Hskew. by move/pred_LRtriple_fast_bijLRyam => /=. 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