proposition: Lemma eocat_tetake_totake (T : eqType) n (t : (n + n).-tuple T) : t = teocat (tetake t) (totake t).
proof: Proof. by apply/val_eqP; rewrite /= (@eocat_etake_otake T n) // size_tuple. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)