proposition: Lemma eotcat_nseq (A : Type) (a : A) n m : m <= n <= m.+1 -> eotcat (nseq n a) (nseq m a) = nseq (n + m) a.
proof: Proof. elim: n m => [[]//|n IH [|m]]; first by case: (n). rewrite addnS /= !ltnS => H. by rewrite IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort