proposition: Lemma sorted_drop (s : seq T) m : sorted leT s -> sorted leT (drop m s).
proof: Proof. by elim: s m => //= a l ih [|n h] //; apply/ih/(path_sorted 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)