proposition: Lemma behead_nseq {n A} (a:A) : behead_tuple (nseq_tuple n.+1 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)