proposition: Lemma LRsupport_conj (T1 : stdtabn d1) (T2 : stdtabn d2): LRsupport (conj_stdtabn T1) (conj_stdtabn T2) = (@conj_stdtabn _) @: (LRsupport T1 T2).
proof: Proof. Proof using . apply/setP => T; rewrite inE. apply/idP/idP. - rewrite -LRtriple_fastE; try exact: is_stdtab_conj => //; last exact: stdtabnP. move=> H. apply/imsetP; exists (conj_stdtabn T). + rewrite inE -LRtriple_fastE //. rewrite pred_LRtriple_conj // conj_tabK; first exact H. * exact: stdtabP. * apply val_inj; rewrite /= conj_tabK //; exact: stdtabP. - move=> /imsetP[U]; rewrite inE -LRtriple_fastE //. rewrite pred_LRtriple_conj // => H ->{T}. rewrite -LRtriple_fastE; try exact: is_stdtab_conj. exact: H. 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