proposition: Lemma sorted_take (s : seq T) m : sorted leT s -> sorted leT (take m s).
proof: Proof. move=> H; exact: (subseq_sorted leT_tr (subseq_take _ _) H). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)