proposition: Theorem eq_inv_is_skew_tableau_reshape inner outer (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : size inner <= size outer -> eq_inv u1 u2 -> size u1 = sumn (outer / inner) -> is_skew_tableau inner (skew_reshape inner outer u1) -> is_skew_tableau inner (skew_reshape inner outer u2).
proof: Proof. rewrite (is_skew_tableau_skew_reshape_pad0 _ _ u1). rewrite (is_skew_tableau_skew_reshape_pad0 _ _ u2). move=> Hleq Hinv Hsz. apply eq_inv_is_skew_tableau_reshape_size. - elim: outer inner Hleq {Hsz} => [| out0 out IHout] [| inn0 inn] //=. + by rewrite size_nseq. + by rewrite ltnS subSS => /IHout /= ->. - exact Hinv. - by rewrite diff_shape_pad0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab