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