proposition: Lemma etake_eotake (A : Type) d n (s : seq A) : n < `2^ d -> etake (eotake d n s) = eotake d.+1 n s.
proof: Proof. have IH0 d1 l1 : etake (eotake d1 0 l1) = eotake d1.+1 0 l1. elim: d1 l1 => [//|d1 IH l1]. by rewrite !(eotakeS d1.+1) -[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 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. by rewrite !(eotakeS d.+1) [LHS]/=; case: odd; apply: IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort