proposition: Lemma perm_KostkaMon m1 m2 : perm_eq m1 m2 -> KostkaMon m1 = KostkaMon m2.
proof: Proof. move=> /tuple_permP[s /val_inj Hs]. suff: Posz (KostkaMon m1) = Posz (KostkaMon m2) by move => []. rewrite -!natz -!(Kostka_Coeff _ (Multinom _)). set mu1 := Multinom m1. set mu2 := Multinom m2. have {Hs} -> : mu1 = [multinom mu2 (s i) | i < n.+1]. apply val_inj => /=; rewrite Hs. by apply eq_from_tnth => i; rewrite tnth_mktuple. by rewrite -mcoeff_sym (issymP _ (Schur_sym _ _ _)). 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