proposition: Lemma ext_tab_subproof t : is_tab_of_shape mu (ext_tab_fun t).
proof: Proof. rewrite /ext_tab_fun. case: (boolP (eqeval t s)) => [/= Hev |_]; last by case: (locked _). have Hincl:= hb_strip_included Hstrip. apply/andP; split. - apply join_tab_skew => //. + rewrite to_word_skew_reshape // ?size_nseq ?sumndiff //. apply/allP => /= i /nseqP[->{i} Hsm]. apply/allP => /= i /count_memPn/eqP Hi. rewrite ltEord /=. move: Hi; apply contraR; rewrite -leqNgt => Hi. by rewrite (eqevalP _ (ltnW Hsz) Hev) nth_default. + have:= Hstrip; rewrite -(hb_strip_rowE (u := nseq m sz)) => //. * by rewrite Hincl /= shape_tabsh. * apply/(is_rowP ord0) => i j; rewrite size_nseq => /andP[Hij Hj]. by rewrite !nth_nseq Hj (leq_ltn_trans Hij Hj). * by rewrite size_nseq sumndiff. - rewrite -(shape_tabsh t) shape_join_tab_skew_reshape ?shape_tabsh //. by rewrite size_nseq sumndiff. 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