proposition: Lemma etake_cat (T : Type) (s1 s2 : seq T) : etake (s1 ++ s2) = etake s1 ++ if odd (size s1) then otake s2 else etake s2.
proof: Proof. have [n leMs1] := ubnP (size s1). elim: n s1 leMs1 => // n IH [|a[|b s1]] //= slLn. by rewrite negbK IH // -ltnS (leq_trans _ slLn). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)