proposition: Lemma to_word_skew_reshape inner outer s : included inner outer -> size s = sumn (outer / inner) -> to_word (skew_reshape inner outer s) = s.
proof: Proof. Proof using. rewrite /skew_reshape /to_word revK. 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 flatten_rcons IHout; first by rewrite cat_take_drop. 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 flatten_rcons IHinn. - by rewrite cat_take_drop. - exact: Hincl. - by rewrite sumn_rev size_takel // Hsz leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab