proposition: Lemma eotcat_take (A : Type) d n (s : seq A) : n < `2^ d -> eotcat (eotake d.+1 n s) (eotake d.+1 (`2^ d + n) s) = eotake d n s.
proof: Proof. move=> nL2d. have IH0 d1 s1 : eotcat (eotake d1.+1 0 s1) (eotake d1.+1 (`2^ d1) s1) = eotake d1 0 s1. elim: d1 s1 => [/= s1|d1 IH s1]; first by rewrite eotcatK. rewrite !(eotakeS d1.+1). by rewrite [RHS]/= -[RHS]IH /= addnn odd_double doubleK. 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. rewrite !(eotakeS d.+1) [X in odd(X + _)]addnn oddD odd_double addFb [RHS]/=. have -> : (`2^ d.+1 + n)./2 = `2^d + n./2. by rewrite /= addnn halfD doubleK odd_double. rewrite -(odd_double_half n) in nLm nLd. case: (boolP (odd n)) nLm nLd; rewrite ?(addSn, add0n, ltnS) => nO nLm nLd. apply: IH => //. by rewrite (leq_ltn_trans _ nLm) // -addnn leq_addr. by rewrite -ltn_double -[X in _ < X]addnn (leq_ltn_trans _ nLd). case: (ltngtP 0 n) => // [n_gt0|<-]; last by rewrite addn0 IH0. apply: IH => //. case: (n) nO n_gt0 nLm => // [] [|n1] //= _ _ n1Lm. by rewrite (leq_trans _ n1Lm) // -addnn addnS addSn !ltnS leq_addr. by rewrite -ltn_double -[X in _ < X]addnn (leq_ltn_trans _ nLd). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort