proposition: Theorem LRtab_coeff_shapeE (T1 : stdtabn d1) (T2 : stdtabn d2) P : shape T1 = P1 -> shape T2 = P2 -> LRtab_coeff P = #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
proof: Proof. Proof using . rewrite /LRtab_coeff /LRtab_set => H1 H2. by apply card_LRtab_set_shapeE; rewrite shape_hyper_stdtabnP ?H1 ?H2. 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