proposition: Lemma map_pairmap {T T0 T1 : Type} (f : T0 -> T1) (g : T -> T -> T0) (s : seq T) (x0 : T) : map f (pairmap g x0 s) = pairmap (fun x y => f (g x y)) x0 s.
proof: Proof. elim: s x0 => [| h s IH] x0 //=. by rewrite IH. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)