proposition: Lemma etake_sorted (leA : rel A) (s : seq A) : transitive leA -> sorted leA s -> sorted leA (etake s).
proof: Proof. move=> leA_trans. have [n leMs] := ubnP (size s). elim: n s leMs => // k IH [|a [|b [| c s]]] // H1 H2. rewrite /= in H2; have /and3P[aLb bLc cPs] := H2. suff : leA a c && sorted leA (etake (c :: s)) by []. rewrite (leA_trans _ _ _ aLb bLc) // IH //=. by rewrite /= ltnS in H1; rewrite (leq_ltn_trans _ H1). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)