proposition: Theorem LRtab_coeffP : Schur P1 * Schur P2 = \sum_P (Schur P) *+ LRtab_coeff P.
proof: Proof. Proof using . rewrite /LRtab_coeff /LRtab_set. have:= LR_rule_tab (hyper_stdtabn P1) (hyper_stdtabn P2). rewrite !shaped_hyper_stdtabnP => ->. move : (LRsupport _ _) => LR. rewrite (partition_big (@shape_deg (d1 + d2)) predT) //=. apply: eq_bigr => P _. under eq_bigr => T /andP[_ /eqP ->] do []. rewrite sumr_const; congr (_ *+ _). by apply: eq_card => i /=; rewrite unfold_in inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly