proposition: Lemma free_LR_rule : catlang (freeSchur Q1) (freeSchur Q2) = \bigcup_(Q in LRsupport) freeSchur Q.
proof: Proof. Proof using . rewrite /catlang. apply/setP/subset_eqP/andP; split; apply/subsetP=> t. - move/imset2P => [w1 w2]. rewrite !freeSchurP /= => Hw1 Hw2 ->. have:= conj Hw1 Hw2. rewrite LRtriple_cat_equiv // => [[H1 H2] [Q [Htriple /= Hcat]]]. have:= is_stdtab_of_n_LRtriple (stdtabnP Q1) (stdtabnP Q2) Htriple. rewrite !size_tab_stdtabn => HQ. apply/bigcupP; exists (StdtabN HQ). rewrite /LRsupport inE -LRtriple_fastE //. apply/LRtripleP => //; exact: Htriple. by rewrite freeSchurP. - move/bigcupP => [Q]; rewrite /LRsupport freeSchurP inE => Htriple /= Ht. have Hsz1 : size (take d1 t) == d1. by rewrite size_takel // size_tuple leq_addr. pose t1 := Tuple Hsz1. have Hsz2 : size (drop d1 t) == d2. by rewrite size_drop size_tuple addKn. pose t2 := Tuple Hsz2. have Hcat : t = cat_tuple t1 t2. by apply: val_inj => /=; rewrite cat_take_drop. have : val t1 \in langQ Q1 /\ val t2 \in langQ Q2. rewrite LRtriple_cat_equiv // !size_tuple !size_tab_stdtabn //. split; try by []. exists Q; split. + by apply/LRtripleP => //; rewrite LRtriple_fastE. + by rewrite /= cat_take_drop. move=> [/= Ht1 Ht2]. apply/imset2P; apply: (Imset2spec (x1 := t1) (x2 := t2)). + by rewrite freeSchurP. + by rewrite freeSchurP. + by apply: val_inj; rewrite /= cat_take_drop. 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