proposition: Lemma Kostka_rec_size0 la mu : size la > size mu -> Kostka_rec la mu = 0.
proof: Proof. elim: mu la => [|m mu IHmu] la /= H; first by case: la H. rewrite sumn_map_condE; apply big1 => nu Hnu. by apply IHmu; have := hb_strip_size Hnu => /andP[_ /(leq_trans H)]. 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