proposition: Lemma Sch_size w : size (Sch w) <= size w.
proof: Proof. Proof using. elim/last_ind: w => [// | w wn IHw]; rewrite Sch_rcons size_rcons. exact: (leq_trans (size_ins_sup _ wn)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab