proposition: Lemma Kostka_recE d (la : 'P_d) mu : sumn mu = d -> Kostka_rec la mu = Kostka la mu.
proof: Proof. elim: mu d la => [| m0 mu IHmu] d la /= Hd. subst d; have -> : la = rowpartn 0 by rewrite !intpartn0. by rewrite -rowpartn0E Kostka_diag eqxx. rewrite sumn_map_condE -enum_intpartnE big_map enumT. by rewrite Kostka_ind //; apply eq_big => //= nu Hstrip; apply IHmu. 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