proposition: Lemma etake_cat_nseq (T : Type) (a1 a2 : T) m1 m2 : etake (nseq m1 a1 ++ nseq m2 a2) = nseq (uphalf m1) a1 ++ nseq (~~odd m1 + m2)./2 a2.
proof: Proof. by rewrite etake_cat !etake_nseq otake_nseq size_nseq; case: (odd m1). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)