proposition: Theorem LRtab_coeffP : Schur P1 * Schur P2 = \sum_(P : 'P_(d1 + d2) | included P1 P) Schur P *+ LRcoeff P1 P2 P.
proof: Proof. Proof using . rewrite (LRyam_coeffP P1 P2). by apply eq_bigr => outer /LRcoeffE ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule mathcomp(ssralg)