proposition: Lemma nth_zip_cond p s t i : nth p (zip s t) i = (if i < size (zip s t) then (nth p.1 s i, nth p.2 t i) else p).
proof: Proof. rewrite size_zip ltnNge geq_min. by elim: s t i => [|x s IHs] [|y t] [|i] //=; rewrite ?orbT -?IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)