proposition: Lemma nth_zip x y s t i : size s = size t -> nth (x, y) (zip s t) i = (nth x s i, nth y t i).
proof: Proof. by elim: i s t => [|i IHi] [|y1 s1] [|y2 t] //= [/IHi->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)