proposition: Lemma eocat_nseq_catD (T : Type) (v1 v2 : T) a b c : eocat (nseq a v1 ++ nseq b v2) (nseq a v1 ++ nseq c v2) = (nseq (a + a) v1 ++ nseq (b + b) v2).
proof: Proof. elim: a b c => // [b c | n IH b c]; first by rewrite eocat_nseqD. by rewrite addnS /= IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)