proposition: Lemma otake_eotake (A : Type) d n (s : seq A) : n < `2^ d -> otake (eotake d n s) = eotake d.+1 (`2^ d + n) s.
proof: Proof. have IH0 d1 s1 : otake (eotake d1 0 s1) = eotake d1.+1 (`2^ d1) s1. elim: d1 s1 => [//=|d1 IH s1]. rewrite !(eotakeS d1.+1) [X in odd X]/= addnn odd_double. by rewrite [X in X./2]addnn doubleK -[RHS]IH. move=> nL2d. have [m leMn] := ubnP n. elim: m n d s leMn nL2d => [[]//|m IH n [|d] s nLm nLd]. by case: (n) nLd => //= _; apply: eotcatK. case: (ltngtP 0 n) => // [n_gt0|<-]; last by rewrite addn0 IH0. have n2Ld : n./2 < `2^ d. rewrite -ltn_double -[X in _ < X]addnn (leq_ltn_trans _ nLd) //. by rewrite -[X in _ <= X](odd_double_half n) leq_addl. have n2Lm : n./2 < m. case: (n) n_gt0 nLm => // [] [|m1] //= _. rewrite -(odd_double_half m1.+2) /= doubleS addnS ltnS. move => /(leq_ltn_trans _)->//. by rewrite addnS ltnS -addnn addnA leq_addl. have HE : (`2^ d.+1 + n)./2 = `2^ d + n./2. by rewrite halfD odd_e2 /= addnn doubleK. rewrite !(eotakeS d.+1) oddD odd_e2 HE. rewrite -IH // [LHS]/=. by case: odd => //=; rewrite IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort