proposition: Lemma eval_res_tab (t : Tm) : shape (filter_gt_tab sz t) == la -> eqeval t (rcons s m) -> eqeval (res_tab t) s.
proof: Proof. move=> Hsh Hev ; rewrite /res_tab (insubT _ (res_tabP Hsh)) /=. apply/eqevalP; first exact: ltnW. move=> i /=; rewrite -filter_gt_to_word. case: (ssrnat.ltnP i sz) => Hisz. - move: Hev => /(eqevalP _ Hszrcons)/(_ i). rewrite nth_rcons Hisz => <-. elim: (to_word t) => //= w0 w IHw. case: ltP; rewrite /= IHw //= /eq_op /=. rewrite leEord /= => /(leq_trans Hisz)/gtn_eqF => ->. by rewrite add0n. - rewrite nth_default //. apply/count_memPn; rewrite mem_filter /=. by rewrite ltEord /= ltnNge Hisz. 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