proposition: Corollary size_ndec_Sch w s : subseqrow s w -> (size s) <= size (Sch w).
proof: Proof. Proof using. case/lastP: s => [// | s si]. move/Sch_leq_last => [H _]. by rewrite size_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab