proposition: Lemma exp1sumnDsize la : (-1) ^+ (d - size la) = \prod_(i <- la) (-1) ^+ i.+1 :> R.
proof: Proof. case: la => [la /= /andP[/eqP <-]]. elim: la => [/= | l0 la IHla] Hpart; first by rewrite subnn expr0 big_nil. have /= l0ne0 := part_head_non0 Hpart. have /= Hla := size_part Hpart. move: Hpart => /= /andP[_ Hpart]. rewrite big_cons -(IHla Hpart) {IHla}. rewrite -expri2 subnS prednK ?subn_gt0 // -subSn; last exact: ltnW. by rewrite -addSn -exprD addnBA // size_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv