proposition: Lemma nth_pairmap s n : n < size s -> forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).
proof: Proof. by elim: s n => [|y s IHs] [|n] //= Hn x; apply: IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)