proposition: Theorem LRyam_coeffE : LRtab_coeff P1 P2 P = LRyam_coeff.
proof: Proof. Proof using Hincl. rewrite /LRtab_coeff /LRyam_coeff. suff -> : LRtab_set P1 P2 P = bijLR @: LRyam_set. by apply card_in_imset; apply bijLR_inj. exact: bijLR_image. 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