proposition: Lemma eval_ext_tab (t : T) : eqeval t s -> eqeval (ext_tab t) (rcons s m).
proof: Proof. move=> Hev; apply/eqevalP; first by rewrite size_rcons. move=> i; rewrite /= /ext_tab_fun Hev /=. have Hszle : size t <= size (skew_reshape la mu (nseq m sz)). rewrite size_skew_reshape. by apply: (leq_trans _ Hlamu); rewrite -(shape_tabsh t) size_map. move: Hszle => /perm_join_tab/seq.permP ->. rewrite count_cat (eqevalP _ (ltnW Hsz) Hev). rewrite to_word_skew_reshape ?size_nseq ?sumndiff ?hb_strip_included //. rewrite count_nseq /= nth_rcons /= {1}/eq_op /=. case: (ssrnat.ltnP i (size s)) => [/gtn_eqF ->| H]. by rewrite mul0n addn0. rewrite (nth_default _ H) add0n eq_sym. by case: eqP => _; rewrite ?mul0n ?mul1n. 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