proposition: Lemma filter_ext_tab (t : T) : eqeval t s -> filter_gt_tab sz (ext_tab t) = t.
proof: Proof. move=> Hev. rewrite /ext_tab /ext_tab_fun /= Hev. rewrite [map _ (join_tab _ _)](_ : _ = pad [::] (size mu) t). - rewrite /pad filter_cat {Hev}. rewrite [X in _ ++ X](eq_in_filter (a2 := pred0)); first last. by move=> x /nseqP[->]. rewrite filter_pred0 cats0. case: t => t /= /andP[Ht _]. by elim: t Ht => //= t0 t IHt /and4P[-> _ _ /IHt] /= ->. - have Hszle : size t <= size mu. by apply: (leq_trans _ Hlamu); rewrite -(shape_tabsh t) size_map. apply (eq_from_nth (x0 := [::])). rewrite /join_tab !size_map size_zip !size_cat !size_nseq. by rewrite size_skew_reshape subnKC // minnn. move=> i; rewrite size_map => Hi. rewrite (nth_map [::]) // nth_cat nth_nseq if_same. move: Hi; rewrite /join_tab size_map => Hi. rewrite /join_tab (nth_map ([::], [::])) // nth_zip /=; first last. by rewrite size_skew_reshape size_cat size_nseq subnKC. rewrite filter_cat nth_cat. have Hfil : [seq x <- nth [::] (skew_reshape la mu (nseq m sz)) i | (x < sz)%O] = [::]. apply/nilP; rewrite /nilp size_filter. rewrite (eq_in_count (a2 := pred0)) ?count_pred0 // => x /=. case: (ssrnat.ltnP i (size (skew_reshape la mu (nseq m sz)))) => [|Hi1]; last by rewrite nth_default. rewrite /skew_reshape size_rev => Hi1; rewrite nth_rev //. rewrite nth_reshape => /mem_take/mem_drop/nseqP[-> _]. by rewrite ltxx. case: (ssrnat.ltnP i (size t)) => {}Hi; first last. by rewrite Hfil nth_nseq if_same. rewrite Hfil cats0 (eq_in_filter (a2 := predT)) ?filter_predT //. move=> x /count_memPn/eqP Hcount. rewrite ltEord /=. suff : nth 0 s x != 0. by case: ssrnat.ltnP => // H; rewrite nth_default. rewrite -(eqevalP t (ltnW Hsz) Hev x). rewrite /to_word seq.count_flatten map_rev sumn_rev sumnE. rewrite (big_nth 0) size_map big_mkord /= (bigD1 (Ordinal Hi)) //=. rewrite (nth_map [::]) //. by move: Hcount; apply contra; rewrite addn_eq0 => /andP[]. 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