proposition: Lemma stdtabsh_eval_to_word (t : stdtabsh la) : eval [seq inord i | i <- to_word t] = td.
proof: Proof. apply/eq_from_tnth => i. case: t => /= t /andP[/andP[Ht Hstd] /eqP Hsh]. rewrite /eval !tnth_mktuple. move: Hstd; rewrite /is_std. rewrite size_to_word /size_tab Hsh sumn_intpartn => Hstd. rewrite count_map (eq_in_count (a2 := pred1 (i : nat))); first last. move=> /= j; rewrite (perm_mem Hstd) mem_iota /= add0n. move => /leq_trans /(_ Hd) Hj. by rewrite {1}/eq_op /= inordK. by rewrite (seq.permP Hstd) count_uniq_mem ?iota_uniq // mem_iota /= add0n. 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