proposition: Corollary zip_mapl {P Q R} (f : P -> R) (s1 : seq P) (s2 : seq Q) : zip (map f s1) s2 = map (fun '(x1,x2) => (f x1,x2)) (zip s1 s2).
proof: Proof. by rewrite -{1}(map_id s2) zip_map2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)