proposition: Lemma skew_reshapeK inner t : size inner <= size t -> skew_reshape inner (outer_shape inner (shape t)) (to_word t) = t.
proof: Proof. Proof using. rewrite -(size_map size) => H. by rewrite /skew_reshape (outer_shapeK H) -shape_rev flattenK revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab