proposition: Lemma syms_symm_int la : 's[la] = \sum_(mu : 'P_d) 'K(la, mu)%:R *: 'm[mu] :> SF.
proof: Proof. rewrite /Kostka; apply val_inj; rewrite /= linear_sum /=. apply mpolyP => m; rewrite Kostka_Coeff linear_sum /=. case/altP: (mdeg m =P sumn la) => Heq; first last. - rewrite (KostkaMon_sumeval Heq); symmetry; apply big1 => i _. rewrite mcoeffZ. case: (leqP (size i) n.+1) => [Hszl | /symm_oversize ->]; first last. by rewrite mcoeff0 mulr0. rewrite mcoeff_symm //=. rewrite [perm_eq _ _](_ : _ = false) /= ?mulr0 //; apply/negP => /perm_sumn. rewrite !sumnE -!/(mdeg _) -sumn_partm mpartK // sumn_intpartn => Habs. by move: Heq; rewrite sumn_intpartn Habs eq_refl. - have Hpm : is_part_of_n d (partm m). by rewrite /= sumn_partm Heq sumn_intpartn eq_refl /=. rewrite (bigD1 (IntPartN Hpm)) //= big1 ?addr0. + rewrite mcoeffZ (mcoeff_symm _ _ (size_partm _)). rewrite perm_sym partm_permK /= mulr1. congr _%:R. rewrite -Kostka_any ?leqSpred // [RHS](Kostka_any _ (size_partm m)). by apply perm_KostkaMon; apply: partm_permK. + move=> mu Hmu; rewrite mcoeffZ. case: (leqP (size mu) n.+1) => [Hszl | /symm_oversize ->]; first last. by rewrite mcoeff0 mulr0. rewrite mcoeff_symm //=. suff /negbTE -> : ~~ (perm_eq (mpart (n := n.+1) mu) m) by rewrite mulr0. move: Hmu; apply contra => /perm_partm H. apply/eqP/val_inj => /=; rewrite -H. by rewrite mpartK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv