proposition: Theorem LR_rule_tab : Schur (shape_deg Q1) * Schur (shape_deg Q2) = \sum_(Q in LRsupport) (Schur (shape_deg Q)).
proof: Proof. Proof using . rewrite !Schur_freeSchurE catlangM free_LR_rule. rewrite -cover_imset /polylang. rewrite big_trivIset /=; first last. apply/trivIsetP => S1 S2. move => /imsetP[/= T1]; rewrite inE => HT1 ->{S1}. move => /imsetP[/= T2]; rewrite inE => HT2 ->{S2}. rewrite /freeSchur => Hdiff. rewrite /disjoint; apply/pred0P => w /=. rewrite !inE; apply: negbTE; move: Hdiff; apply: contra. by move=> /andP[/eqP-> /eqP->]. under [RHS]eq_bigr do rewrite Schur_freeSchurE. rewrite (big_setID [set set0]) /= big1 ?add0r; first last => [i|]. rewrite inE => /andP[_]; rewrite inE => /eqP ->. by rewrite big_set0. rewrite (big_setID [set x | freeSchur x == set0]) /=. rewrite [X in X + _]big1 ?add0r; first last => [i|]. rewrite inE => /andP[_]; rewrite inE => /eqP ->. by rewrite /polylang big_set0. rewrite -big_imset /=; first last => [T1 T2 /=|]. rewrite inE => /andP[]; rewrite inE => /set0Pn [x1 Hx1] _ _. move: Hx1; rewrite inE => /eqP Hx1 /setP/(_ x1); rewrite !inE Hx1. rewrite eq_refl => /esym/eqP; exact: val_inj. apply: eq_bigl => s; rewrite !inE; apply/idP/idP. + move=> /andP[Hn0 /imsetP[Q HQ Hs]]; subst s. by rewrite imset_f //= inE HQ inE Hn0. + move/imsetP => [Q]; rewrite 2!inE => /andP[H1 H2] ->. by rewrite H1 /= imset_f. 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