From 273e12e9e4eb2a18289f404f0ec41db71af88624 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 23 Aug 2019 10:26:42 +0200
Subject: [PATCH] Add `map_zip_with_flip`.

---
 theories/fin_maps.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 19251236..d7b147cf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1369,6 +1369,13 @@ Proof.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
 
+Lemma map_zip_with_flip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
+  map_zip_with (flip f) m2 m1 = map_zip_with f m1 m2.
+Proof.
+  apply map_eq; intro i. rewrite !map_lookup_zip_with.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
 Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) :
   map_zip_with f m1 m2 = curry f <$> map_zip m1 m2.
 Proof.
-- 
GitLab