proposition: Lemma size_etake (T : Type) (s : seq T) : size (etake s) = uphalf (size s).
proof: Proof. have [n leMn] := ubnP (size s); elim: n s leMn => // n IH [|a [|b s]] //=. rewrite !ltnS => slLn. by rewrite IH //= (leq_trans _ slLn). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)