proposition: Lemma Newton_syme1 (k : nat) : k%:R *: 'e_k = \sum_(1 <= i < k.+1) (-1) ^+ i.+1 *: 'p_i * 'e_(k - i) :> SF.
proof: Proof. Proof using. case: k => [|[|k]]; first by rewrite scale0r big_nil. rewrite scale1r /index_iota big_cons big_nil addr0. by rewrite subnn syme0 sympe1E mulr1 -(expr1 (-1)) sqrr_sign scale1r. rewrite big_nat_recl // -(expr1 (-1)) sqrr_sign scale1r. rewrite subn1 /= mulrC mul_ek_p1 -[LHS]addr0 -addrA; congr (_ + _). apply esym; rewrite big_add1 /=. rewrite big_nat_recr //= subnn syme0 mulr1 expr1 expri2. rewrite big_nat (eq_bigr (fun i => (-1) ^+ i.+1 *: 'm[hookpartn k.+2 i.+2] - (-1) ^+ i *: 'm[hookpartn k.+2 i.+1])); first last. move=> i /= ltin; rewrite expri2 -scaleNr -(mulrN1 ((-1) ^+ i)) -exprSr. rewrite -scalerDr -scalerAl; congr (_ *: _). by rewrite subSS subSn // mulrC mul_ek_pk -addnS subnK // addrC. rewrite -big_nat telescope_sumr // expr0 scale1r. rewrite [_ - _]addrC !addrA subrr add0r. rewrite exprS mulN1r scaleNr -scalerBr. by rewrite hookpartn_row -symp_to_symm subrr scaler0. 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