fact: Fixpoint Kostka_rec (la mu : seq nat) : nat := if mu is m :: mu then sumn [seq Kostka_rec nu mu | nu <- enum_partn (sumn mu) & hb_strip nu la] else la == [::].
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