proposition: Lemma tab_eval_partdom (t : tabsh la) : partdom (eval (to_word t)) la.
proof: Proof. apply/partdomP => i; rewrite -(shape_tabsh t). case: (ssrnat.leqP i n.+1) => [Hi| /ltnW Hi]; first last. rewrite !take_oversize ?size_tuple //; first last. by rewrite size_map (leq_trans (size_tabsh _)). by rewrite sumn_eval size_to_word. rewrite sumn_take big_mkord (big_ord_widen _ _ Hi). under eq_bigr do rewrite (nth_map ord0) ?size_enum_ord // nth_ord_enum. rewrite sum_count_mem /= /to_word seq.count_flatten map_rev sumn_rev. rewrite -{1}(cat_take_drop i t) map_cat sumn_cat addnC. rewrite sumnE big_map big_seq big1 ?add0n; first last. move=> /= s Hs; rewrite -(nth_index [::] Hs). rewrite nth_drop; apply/eqP; rewrite -leqn0 leqNgt -has_count -all_predC. under eq_all => j /= do rewrite -leqNgt. have:= all_ltn_nth_tabsh t (i + index s (drop i t)); apply sub_all. by move=> j; apply (leq_trans (leq_addr _ _)). rewrite /shape -map_take !sumnE !big_map. by apply leq_sum => /= j _; apply: count_size. 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