proposition: Lemma etake_tupleP m (T : Type) (t : (m + m).-tuple T) : size (etake t) == m.
proof: Proof. by rewrite size_etake size_tuple /= addnn uphalf_double. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)