proposition: Lemma card_LRtab_set_shapeE P (U1 T1 : stdtabn d1) (U2 T2 : stdtabn d2) : shape T1 = shape U1 -> shape T2 = shape U2 -> #|[set Q in (LRsupport U1 U2) | (shape Q == P)]| = #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
proof: Proof. Proof using . by move=> H1 H2; apply anti_leq; rewrite !card_LRtab_set_leq // 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