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