proposition: Lemma omegasf_symp i : 0 < i <= n -> omegasf 'p_i = (-1) ^+ i.+1 *: 'p_i.
proof: Proof. rewrite andbC => /andP[lein]. have [j] := ubnPgeq i; elim: i lein j => [//| i IHi] /= ltin j. by move=> /(leq_trans _) /[apply]. move=> H1 lt0j; move: H1. rewrite leq_eqVlt orbC => /orP[/IHi ->// | /eqP->{j lt0j}]; first exact: ltnW. move/(_ (ltnW ltin)) in IHi. have := Newton_symh1 n0 R i.+1. rewrite big_nat_recr //= subnn symh0 mulr1 addrC => /eqP. have /= <- := subr_eq _ 'p_i.+1 => /eqP {1}<-. rewrite linearP linearN linear_sum /= omegasf_symh //. rewrite big_nat; under eq_bigr => j /andP[lt0j ltji1]. by rewrite rmorphM /= IHi // omegasf_symh ?(leq_trans (leq_subr _ _)) // over. rewrite -big_nat (Newton_syme1 n0 R i.+1). rewrite big_nat_recr //= [X in X - _]addrC addrK. by rewrite subnn syme0 mulr1. 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