proposition: Lemma otake_sorted (leA : rel A) (s : seq A) : transitive leA -> sorted leA s -> sorted leA (otake s).
proof: Proof. move=> leT_trans; case: s => //= a s sS. by apply: etake_sorted => //; case: s sS => //= b l /andP[]. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)