proposition: Lemma KostkaInv_unitrig d : unitrig (fun la mu : 'PDom_d => KostkaInv la mu).
proof: Proof. exact: (Minv_unitrig (Kostka_unitrig _ d)). 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