proposition: Lemma Newton_symh1 (k : nat) : k%:R *: 'h_k = \sum_(1 <= i < k.+1) 'p_i * 'h_(k - i) :> SF.
proof: Proof. Proof using. rewrite Newton_symh big_mkord (reindex_inj rev_ord_inj) /=. rewrite big_add1 /= big_mkord; apply eq_bigr => i _. by rewrite mulrC subKn. 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