proposition: Lemma shape_res_tab_subproof (t : Tm) : is_part_of_n (sumn s) ( if eqeval t (rcons s m) then shape (filter_gt_tab sz t) else locked rowpartn (sumn s)).
proof: Proof. case: (boolP (eqeval t (rcons s m))) => Hev /= ; last by case: (locked _). apply/andP; split. - apply/eqP. rewrite -/(size_tab _) -size_to_word -filter_gt_to_word size_filter. rewrite -sum_count_mem /=. transitivity (\sum_(i < n.+1 | i < sz) nth 0 s i). apply eq_big => i; rewrite ltEord//= => Hi. by rewrite (eqevalP _ Hszrcons Hev) nth_rcons Hi. rewrite sumnE (big_nth 0) big_mkord /=. by apply esym; apply big_ord_widen; apply ltnW. - by apply: is_part_sht; 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