fact: Definition bijLR (yam : yameval P2) : stdtabn (d1 + d2) := if (boolP (is_skew_reshape_tableau P P1 yam)) is AltTrue pf then StdtabN (bijLRyamP pf) else hyper_stdtabn P.
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