proposition: Lemma sumn_eval w : sumn (eval w) = size w.
proof: Proof. rewrite sumnE /eval big_tuple. under eq_bigr do rewrite tnth_mktuple. by rewrite sum_count_mem count_predT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn