proposition: Lemma subseq_take (T : eqType) k (l : seq T) : subseq (take k l) l.
proof: Proof. by rewrite -{2}[l](cat_take_drop k); exact: prefix_subseq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast