proposition: Lemma shape_skew_reshape inner outer s : included inner outer -> size s = sumn (outer / inner) -> shape (skew_reshape inner outer s) = outer / inner.
proof: Proof. Proof using. rewrite /shape /skew_reshape. elim: inner outer s => [| inn0 inn IHinn] /= outer s. move=> _; elim: outer s => [s /eqP/nilP -> // | out0 out IHout] /= s Hsz. rewrite rev_cons reshape_rcons; last by rewrite sumn_rev addnC -Hsz. rewrite rev_rcons /= IHout. - by rewrite size_drop sumn_rev Hsz addnK. - by rewrite sumn_rev size_takel // Hsz leq_addl. case: outer s => [// | out0 out] /= s /andP[H0 Hincl] Hsz. rewrite rev_cons reshape_rcons; last by rewrite sumn_rev addnC -Hsz. rewrite rev_rcons /= size_drop sumn_rev. rewrite (IHinn _ _ Hincl); first by rewrite Hsz addnK. by rewrite size_takel // Hsz leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab