proposition: Lemma res_tabP (t : Tm) : shape (filter_gt_tab sz t) == la -> is_tab_of_shape la (filter_gt_tab sz t).
proof: Proof. rewrite /= andbC => -> /=. by apply: is_tableau_filter_gt; apply tabshP. 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