proposition: Lemma nth_eotake (A : Type) d n (s : seq A) a x : nth a (eotake d n s) x = nth a s ((n %% `2^ d) + `2^ d * x).
proof: Proof. elim: d n s a x => /= [n s a x|d IH n s a x]; first by rewrite modn1 mul1n. case: (boolP (odd n)) => [nO|nE]; rewrite addnn; last first. rewrite IH nth_etake doubleD doubleMl. by rewrite -muln2 muln_modl !muln2 -[in RHS](odd_double_half n) (negPf nE). rewrite IH nth_otake doubleD -addSn doubleMl. rewrite -muln2 muln_modl !muln2. rewrite -[in RHS](odd_double_half n) nO add1n modnS ifN //. apply/negP=> /dvdnP => [] [k H]. by move: (nO); rewrite -[n]odd_double_half nO addSn H -doubleMr odd_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort