proposition: Theorem LRyam_coeffP : Schur P1 * Schur P2 = \sum_(P : 'P_(d1 + d2) | included P1 P) Schur P *+ LRyam_coeff P.
proof: Proof. Proof using . rewrite LRtab_coeffP. rewrite (bigID (fun P : 'P_(d1 + d2) => included P1 P) predT) /=. rewrite [X in _ + X]big1 ?addr0; first last => [P Hincl|]. suff -> : LRtab_coeff P1 P2 P = 0%N by exact: mulr0n. apply/contraNeq: Hincl. rewrite /LRtab_coeff cards_eq0 => /set0Pn [Q]. exact: LRtab_set_included. by apply: eq_bigr => P /LRyam_coeffE ->. 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