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