proposition: Lemma Schur_tabsh_readingE d (sh : 'P_d) : Schur sh = \sum_(t : d.-tuple 'I_n | tabsh_reading sh t) \prod_(i <- t) 'X_i.
proof: Proof. Proof using. rewrite /Schur -big_enum /=. pose prodw := fun w => \prod_(i <- w) 'X_i : {mpoly R[n]}. rewrite -[LHS](big_map (fun t => to_word (val t)) xpredT prodw). rewrite -[RHS](big_map val (tabsh_reading sh) prodw). rewrite -[RHS]big_filter. rewrite (perm_big _ (to_word_enum_tabsh sh)) /=. by rewrite !big_filter !big_map. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau