proposition: Lemma nth_eotake_div (A : Type) d (s : seq A) a n : nth a (eotake d n s) (n %/ `2^ d) = nth a s n.
proof: Proof. by rewrite nth_eotake mulnC addnC -divn_eq. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort