proposition: Lemma card_eq_eval : #|[set t : tabsh['I_n.+1] mu | (eqeval t (rcons s m)) && (shape (filter_gt_tab sz t) == la)]| = #|[set t : tabsh['I_n.+1] la | eqeval t s]|.
proof: Proof. rewrite -(card_in_imset (f := ext_tab)); first last. by move=> /= p1 p2; rewrite /= !inE; apply ext_tab_inj. congr #|pred_of_set _|; apply/setP => t; rewrite !inE. apply/andP/imsetP => [[Hev Hsh] | [tt]]. - exists (res_tab t); rewrite ?inE; first exact: eval_res_tab. by rewrite res_tabK. - rewrite inE => Hev ->{t}; split; first exact: eval_ext_tab. by rewrite filter_ext_tab // shape_tabsh. 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