proposition: Lemma eocat_tupleP (T : Type) m1 m2 (t1 : m1.-tuple T) (t2 : m2.-tuple T) : size (eocat t1 t2) == m1 + m1.
proof: Proof. by rewrite size_eocat size_tuple. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)