proposition: Lemma take_etakeE (T : Type) (s : seq T) : ~~ odd (size s) -> ~~ odd (size s)./2 -> take (size s)./2./2 (etake s) = etake (take (size s)./2 s).
proof: Proof. move=> H1 H2. pose s1 := take (size s)./2 s; pose s2 := drop (size s)./2 s. pose s3 := etake s; pose s4 := otake s. have lE : s = s1 ++ s2 by rewrite cat_take_drop. have ss1E : size s1 = (size s)./2 by rewrite size_take half_gtnn; case: size. rewrite -/s1. rewrite {2}lE etake_cat ss1E (negPf H2). rewrite take_cat size_etake ss1E. by rewrite uphalf_half (negPf H2) /= ltnn subnn take0 cats0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)