proposition: Lemma tsumnE : tsumn =1 sumn.
proof: Proof. Proof using . rewrite /tsumn => s; rewrite -(add0n (sumn s)); move: 0 => i. elim: s i => [// | s0 s IHs] i /=. by rewrite IHs addE addnA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule