proposition: Lemma nseqCons {n A} (a:A) : nseq_tuple (S n) a = [tuple of a::nseq_tuple n a].
proof: Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth a). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)