proposition: Lemma symHE_rec (d : nat) : d != 0%N -> E d = \sum_(1 <= i < d.+1) H i * ((-1) ^+ i.-1 *: E (d - i)).
proof: Proof. move=> Hd; have:= Hanti Hd. rewrite big_nat_recl // expr0 scale1r H0 mul1r subn0 => /eqP. rewrite (addr_eq0 (E d)) => /eqP ->; rewrite big_add1 /= -sumrN. rewrite !big_nat; apply eq_bigr => i /= Hi. rewrite scalerAr -mulrN; congr (_ * _). rewrite -scaleNr; congr (_ *: _). by rewrite exprS mulN1r opprK. 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