proposition: Lemma Newton_symh (k : nat) : k%:R *: 'h_k = \sum_(0 <= i < k) 'h_i * 'p_(k - i) :> SF.
proof: Proof. Proof using. apply val_inj => /=; apply/mpolyP => m. rewrite mcoeffZ mcoeff_symh !linear_sum big_nat. under eq_bigr => i /= Hi do rewrite mult_symh_powersum subnKC // ?(ltnW Hi) //. rewrite -big_nat -mulr_sumr mulrC. case: (mdeg m =P k) => Hdegm; rewrite /= ?mul1r ?mul0r //. rewrite exchange_big /=. transitivity (\sum_(i < n) (m i)%:R : R). by rewrite -Hdegm mdegE -natr_sum. apply: eq_bigr => i _ /=; rewrite -natr_sum; congr (_%:R). have : m i <= k. by move: Hdegm; rewrite mdegE => <-; rewrite (bigD1 i) //=; apply leq_addr. rewrite big_mkord (reindex_inj rev_ord_inj) /=. under eq_bigr do rewrite subKn //. move: (m i) => n {m Hdegm i} Hn. rewrite (bigID (fun i : 'I_k => i < n)) /=. under eq_bigr => i -> /= do []. rewrite sum_nat_const /= muln1 big1 ?addn0; last by move=> i /negbTE ->. rewrite cardE /= /enum_mem -enumT /=. rewrite (eq_filter (a2 := (preim nat_of_ord (fun i => i < n)))) //. rewrite -(size_map nat_of_ord). by rewrite -filter_map val_enum_ord iota_ltn // size_iota. 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