proposition: Lemma zipCons {n A B} a (aa: n.-tuple A) b (bb: n.-tuple B) : zip_tuple [tuple of a::aa] [tuple of b::bb] = [tuple of (a,b) :: zip_tuple aa bb].
proof: Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth (a,b)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)