diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 19251236bf22bf11a5de0270e4a9a0f75f4aaade..d7b147cf4d057e4280fd99f7dd540ff1065c562e 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.