proposition: Lemma eq_size_eotake (A: Type) d n (s1 s2 : seq A) : size s1 = size s2 -> size (eotake d n s1) = size (eotake d n s2).
proof: Proof. elim: d n s1 s2 => //= d IH n s1 s2 ss1Ess2. case: odd; apply: IH; first by apply: eq_size_otake. by apply: eq_size_etake. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort