proposition: Theorem Sch_max_size (w : seq T) : size (Sch w) = \max_(s : subseqs w | is_row s) size s.
proof: Proof. apply/eqP; rewrite eqn_leq; apply/andP; split. - case: (exist_size_Sch w) => s; rewrite /subseqrow_n => /and3P[Hsubs /eqP Hsz Hrow]. pose witness := Subseqs Hsubs. have -> : size (Sch w) = size witness by rewrite /= Hsz. exact: (@leq_bigmax_cond _ _ (size \o (@subseqsval _ w)) witness Hrow). - apply/bigmax_leqP => s Hs. by apply: size_ndec_Sch; rewrite /subseqrow Hs andbT; apply: subseqsP s. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab