proposition: Lemma size_eocat (T : Type) (s1 s2 : seq T) : size (eocat s1 s2) = (size s1 + size s1).
proof: Proof. by elim: s1 s2 => //= a s1 IH s2; rewrite IH addnS. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)