proposition: Lemma bijLR_image : LRtab_set P1 P2 P = [set bijLR x | x in LRyam_set].
proof: Proof. Proof using . apply setP => Q; apply/idP/idP. - move/bijLR_surj => [y Hy <-]. exact: imset_f. - move/imsetP => [y Hy ->]. rewrite /LRtab_set inE (bijLR_LRsupport Hy) /=. by rewrite shape_bijLR. 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