proposition: Lemma Kostka_Coeff (R : ringType) m : (Schur n R la)@_m = (KostkaMon m)%:R.
proof: Proof. rewrite /Schur linear_sum /= /KostkaMon. rewrite (bigID (fun t : tabsh la => t \in KostkaTab m)) /=. rewrite addrC big1 ?add0r; first last => [i|]. by rewrite /KostkaTab inE evalE => /negbTE ->. under eq_bigr => i do rewrite /KostkaTab inE evalE => /eqP ->; rewrite eqxx. by rewrite sumr_const; congr _%:R; apply eq_card. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn