proposition: Lemma symHE_intcompn d : E d = \sum_(c : intcompn d) (-1)^+(d - size c) *: prod_gen H (partn_of_compn c).
proof: Proof. rewrite symHE_prod_intcomp; apply eq_bigr => c _; congr (_ *: _). rewrite /prod_symh /prod_gen; apply: perm_big. by rewrite perm_sym perm_sort. 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