proposition: Lemma drop_otakeE (T : Type) (s : seq T) : ~~ odd (size s) -> ~~ odd (size s)./2 -> drop (size s)./2./2 (otake s) = otake (drop (size s)./2 s).
proof: Proof. move=> ssE ss2E. pose s1 := take (size s)./2 s; pose s2 := drop (size s)./2 s. pose s3 := etake s; pose s4 := otake s. have sE : s = s1 ++ s2 by rewrite cat_take_drop. have ss1E : size s1 = (size s)./2. by rewrite size_take half_gtnn; case: size. rewrite -/s2. rewrite {2}sE otake_cat ss1E (negPf ss2E). by rewrite drop_cat size_otake ss1E ltnn subnn drop0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)