proposition: Lemma symHE_prod_intcomp d : E d = \sum_(c : intcompn d) (-1) ^+ (d - size c) *: (\prod_(i <- c) H i).
proof: Proof. rewrite -big_enum /=. rewrite -[RHS](big_map (@cnval d) xpredT (fun c : seq nat => (-1)^+(d - size c) *: \prod_(i <- c) H i)). rewrite enum_intcompnE. have [m/ltnW] := ubnP d; elim: m => [| m IHm] in d *. rewrite leqn0 => /eqP ->. by rewrite /enum_compn /= big_seq1 /= subnn expr0 scale1r big_nil E0. rewrite leq_eqVlt => /orP[/eqP Hm|]; last by rewrite ltnS; exact: IHm. rewrite enum_compnE Hm // -Hm big_flatten /=. rewrite symHE_rec; last by rewrite Hm. rewrite big_map /index_iota subSS subn0; apply eq_big_seq => i. rewrite mem_iota add1n ltnS => /andP[Hi Hid]. rewrite big_map. under eq_big_seq => s. rewrite -enum_compnP /is_comp_of_n /= => /andP[/eqP Hsum Hcomp]. rewrite big_cons scalerAr -mulrNN -scaleNr -[- (-1) ^+ _]mulN1r. rewrite -exprS -subSn; first last. rewrite Hm ltnS (leq_trans (size_comp Hcomp)) // {}Hsum. case: i Hi {Hid} => // i' _. by rewrite Hm subSS leq_subr. by rewrite subSS over. rewrite -mulr_sumr. case: (boolP (d - i == 0)%N) => [| Hdi] /=. rewrite subn_eq0 => Hdi. have -> : i = d by apply anti_leq; rewrite Hid Hdi. subst d => /=. rewrite subnn /enum_compn /= big_seq1 big_nil /=. rewrite subn0 E0 mulNr -mulrN -scaleNr; congr (_ * (_)%:A). by rewrite exprS mulN1r opprK. rewrite {}IHm //; first last. rewrite Hm; case: i Hi {Hid Hdi} => // i' _. by rewrite subSS leq_subr. rewrite scaler_sumr mulNr -mulrN -sumrN; congr (_ * _). apply eq_big_seq => s. rewrite -enum_compnP /is_comp_of_n /= => /andP[/eqP Hsum Hn0]. rewrite scalerA -scaleNr; congr (_ *: _). subst d; rewrite -exprD. move: Hdi; rewrite subn_eq0 -leqNgt => {}Hid. rewrite subSn //. case: i Hi Hsum Hid => // i _. rewrite subSS => Hsum Him /=. have Hsz : size s <= m. by apply (leq_trans (size_comp Hn0)); rewrite {}Hsum leq_subr. rewrite -subSn // subSS subSn // exprS mulN1r opprK. rewrite subnAC subnKC //. have:= size_comp Hn0; rewrite Hsum. rewrite -!subn_eq0 !subnBA //; last exact: ltnW. by rewrite addnC. 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