proposition: Corollary exist_size_Sch w : exists s : seq T, subseqrow_n s w (size (Sch w)).
proof: Proof. Proof using. case/lastP: w => [| w wn]; first by exists [::]. have:= size_ins_non_0 (Sch w) wn; rewrite -Sch_rcons. case Hn : (size _) => [_ // | n] _. have:= ltnSn n; rewrite -{2}Hn => H. elim (Sch_exists H) => s /andP[_ Hrsq]. by exists s. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab