proposition: Lemma eotake_mod (A : Type) d n (s : seq A) : eotake d (n %% `2^ d) s = eotake d n s.
proof: Proof. elim: d n s => //= d IH n s; rewrite odd_mod ?(odd_e2 d.+1) //. case: (boolP (odd n)) => [nO|nE]; last first. rewrite -[in LHS](odd_double_half n) (negPf nE) add0n addnn. by rewrite -!muln2 -muln_modl muln2 doubleK IH. rewrite -[in LHS](odd_double_half n) nO add1n modnS. rewrite addnn -!muln2 -muln_modl !muln2 ifN. by rewrite -uphalfE uphalf_half odd_double doubleK IH. 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