proposition: Theorem LRtab_coeff_conj (P1 : 'P_d1) (P2 : 'P_d2) (P : 'P_(d1 + d2)) : LRtab_coeff P1 P2 P = LRtab_coeff (conj_intpartn P1) (conj_intpartn P2) (conj_intpartn P).
proof: Proof. Proof using . rewrite [RHS](LRtab_coeff_shapeE (T1 := conj_stdtabn (hyper_stdtabn P1)) (T2 := conj_stdtabn (hyper_stdtabn P2))); first last. - by rewrite shape_conj_tab shape_hyper_stdtabnP. - by rewrite shape_conj_tab shape_hyper_stdtabnP. rewrite /LRtab_coeff /LRtab_set LRsupport_conj. have Hinj : injective (conj_stdtabn (n:=d1 + d2)). apply inv_inj => T; apply val_inj; rewrite /= conj_tabK //; exact: stdtabP. rewrite -(@card_imset _ _ (@conj_stdtabn _)) //. rewrite !setIdE imsetI; last by move=> a b /= _ _; exact: Hinj. congr (card (mem (_ :&: _))). apply/setP => T; rewrite !inE. apply/idP/idP. - move/imsetP => [U]; rewrite inE => /eqP HU -> /=. by rewrite shape_conj_tab HU. - move/eqP => H; apply/imsetP; exists (conj_stdtabn T). + by rewrite inE /= shape_conj_tab H /= conj_partK. + apply val_inj => //=; rewrite conj_tabK //; exact: stdtabP. 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