proposition: Lemma gtn_size_eotake (A : Type) k p i (s : seq A) : i < `2^ p -> k < size (eotake p i s) -> i + `2^ p * k < size s.
proof: Proof. elim: p i k s => [[]// k s _|p IH i k s iLk kLs]; first by rewrite mul1n. rewrite /= in kLs. case: (boolP (odd _)) kLs => iO /IH; rewrite ?(size_otake, size_etake) ltn_half_double -addnn -e2Sn => /(_ iLk) ikLs. rewrite -(odd_double_half i) iO -addSn -doubleS. rewrite e2Sn addnn -doubleMl -doubleD. rewrite -(odd_double_half (size s)). apply: leq_trans (leq_addl _ _). by rewrite leq_double addSn. move: ikLs. rewrite uphalf_half -[X in i + _ < X](odd_double_half (size s)). rewrite -[i as X in (X + _ < _)]odd_double_half (negPf iO) add0n. rewrite e2Sn addnn -doubleMl -doubleD. case: odd => /=; first by rewrite !ltnS leq_double. by rewrite ltn_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort