proposition: Lemma shape_join_tab_skew_reshape t sh w : included (shape t) sh -> size w = sumn (sh / (shape t)) -> shape (join_tab t (skew_reshape (shape t) sh w)) = sh.
proof: Proof. Proof using. move=> Hincl Hsz. rewrite shape_join_tab size_skew_reshape shape_skew_reshape // {Hsz w}. move: (shape t) Hincl => inner {t}. elim: sh inner => [| s0 sh IHsh] [|in0 inn] //=. rewrite add0n => _ {IHsh}; congr (_ :: _) => {s0}. by elim: sh => //= s0 sh ->. move=> /andP[Hin0 {}/IHsh]; rewrite /pad /= => Hrec. by rewrite subSS (subnKC Hin0) Hrec. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab