proposition: Lemma eocat_cat (T : Type) (s1 s2 s3 s4 : seq T) : ~~ odd (size s1) -> size s1 = size s3 -> eocat (s1 ++ s2) (s3 ++ s4) = eocat s1 s3 ++ eocat s2 s4.
proof: Proof. have [n leMs1] := ubnP (size s1). elim: n s1 s3 leMs1 => //= n IH [|a[|b s1]] [|c[|d s3]] //=. rewrite !ltnS negbK => ss1Ln ss1O [ss1E]. by rewrite IH // (leq_ltn_trans _ ss1Ln). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)