proposition: Lemma hasincr0 : hasincr -> 'a_(mpart la + mesym1 h + rho) = 0%R :> {mpoly R[n]}.
proof: Proof. Proof using . move=> /hasP[i _ /eqP]; exact: alt_add1_0. 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