proposition: Theorem is_skew_tableau_reshape_std inner outer (d : unit) (T : inhOrderType d) (u : seq T) : size inner <= size outer -> size u = sumn (outer / inner) -> is_skew_tableau inner (skew_reshape inner outer u) = is_skew_tableau inner (skew_reshape inner outer (std u)).
proof: Proof. move=> Hin Hsize. apply/idP/idP; apply eq_inv_is_skew_tableau_reshape => //=. - exact: eq_inv_std. - by apply eq_inv_sym; exact: eq_inv_std. - by rewrite size_std. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab