proposition: Lemma is_skew_tableau_skew_reshape_pad0 inner outer (d : unit) (T : inhOrderType d) (u : seq T) : is_skew_tableau inner (skew_reshape inner outer u) = is_skew_tableau ((pad 0 (size outer)) inner) (skew_reshape ((pad 0 (size outer)) inner) outer u).
proof: Proof. rewrite is_skew_tableau_pad0 {1}/skew_reshape size_rev size_reshape size_rev size_diff_shape. congr (is_skew_tableau _ _). by rewrite /skew_reshape diff_shape_pad0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab