proposition: Lemma Kostka_ind d (la : 'P_d) m mu : d = m + sumn mu -> Kostka la (m :: mu) = \sum_(nu : 'P_(sumn mu) | hb_strip nu la) Kostka nu mu.
proof: Proof. case: (leqP (size la) (size mu).+1) => Hszla; first last. move=> _; rewrite Kostka_size0 //. apply esym; apply big1 => nu Hnu; apply Kostka_size0. by have := hb_strip_size Hnu => /andP[_ /(leq_trans Hszla)]. rewrite {1}/Kostka addnC => Hd; subst d. have /permPl/(perm_mpart _)/perm_KostkaMon <- := perm_rcons m mu. rewrite /KostkaMon /KostkaTab. transitivity #|[set t : tabsh['I_(size mu).+1] la | eqeval t (rcons mu m)]|. by apply eq_card. rewrite -sum1dep_card. have Hszmu := ltnSn (size mu). pose sht := @shape_res_tab (size mu) mu m Hszmu la. rewrite (partition_big sht (fun nu : 'P_(sumn mu) => hb_strip nu la)) /=; first last. by move=> t Ht; apply hb_strip_shape_res_tab. apply eq_bigr => /= nu Hstrip; rewrite sum1dep_card. rewrite (Kostka_any _ (ltnW Hszmu)) /KostkaMon /KostkaTab. rewrite -(card_eq_eval _ Hszla Hstrip). apply eq_card => /= t; rewrite !inE. by rewrite -val_eqE /=; case : (eqeval t (rcons mu m)). 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