proposition: Lemma tabsh_is_std (t : tabsh la) : eval (to_word t) = td -> is_std [seq (i : nat) | i : 'I_n.+1 <- to_word t].
proof: Proof. rewrite /is_std => Hev; apply/seq.permP => P. rewrite count_map -sum_count_mem. under eq_bigr => i _. move/(congr1 (fun t => tnth t i)) : Hev; rewrite !tnth_mktuple => ->. by rewrite over. rewrite size_map size_to_word /size_tab shape_tabsh sumn_intpartn. rewrite -sum1_count /= -(big_mkord _ (fun i => i < d : nat)). rewrite -{2}(subn0 d) -/(index_iota 0 d) (big_nat_widen _ _ _ _ _ Hd). rewrite (bigID (gtn d)) /= addnC big1 ?add0n; first last. by move=> i /andP[_ /negbTE ->]. by apply eq_bigr => i /andP[_ ->]. 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