proposition: Lemma is_skew_tableau_pad0 inner t : is_skew_tableau inner t = is_skew_tableau (pad 0 (size t) inner) t.
proof: Proof. Proof using. elim: t inner => [| t0 t IHt] /= inner; first by rewrite cats0. case: inner => [| inn0 inn] /=. rewrite (IHt [::]) /= add0n. by rewrite !subn0. rewrite (IHt inn) subSS /=. suff -> : head 0 (inn ++ nseq (size t - size inn) 0) = head 0 inn by []. by case: inn => //=; case: (size t - 0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition skewpart Yamanouchi ordtype tableau std stdtab