proposition: Lemma leq_size_eotake_e2n (A : Type) i p q (s : seq A) : i <= q -> size s <= `2^ q -> size (eotake i p s) <= `2^ (q - i).
proof: Proof. elim: i p q s => [|i IH] p q s iLq Hs /=; first by rewrite subn0. have q_gt0 : 0 < q by apply: leq_ltn_trans iLq. case: odd. apply: leq_trans (IH _ q.-1 _ _ _) _. - by rewrite -ltnS prednK // (leq_ltn_trans _ iLq). - rewrite size_otake -leq_double -!addnn -e2Sn addnn. rewrite prednK // (leq_trans _ Hs) //. by rewrite -[X in _ <= X]odd_double_half; case: odd. by case: (q) q_gt0. apply: leq_trans (IH _ q.-1 _ _ _) _. - by rewrite -ltnS prednK // (leq_ltn_trans _ iLq). - by rewrite size_etake leq_uphalf_e2n // prednK. by case: (q) q_gt0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort