proposition: Lemma eocat_nseq_catDS (T : Type) (v1 v2 : T) a b : eocat (nseq a.+1 v1 ++ nseq b v2) (nseq a v1 ++ nseq b.+1 v2) = (nseq (a + a).+1 v1 ++ nseq (b + b).+1 v2).
proof: Proof. elim: a b => // [b | a IH b]. by case: b => //= b; rewrite eocat_nseqD [(_ + _)%Nrec]addnS. by rewrite addnS (nseqS a) (nseqS a.+1) 2!(cat_cons v1) eocat_cons IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)