From 4d646c6d5a6cc49c244bfb69ec3758a273dbce09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Jan 2016 18:17:52 +0100
Subject: [PATCH] Lemma about big_opM and delete.

---
 modures/ra.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/modures/ra.v b/modures/ra.v
index bbda7ad82..ad6ce17fe 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -146,6 +146,11 @@ Proof. unfold big_opM. by rewrite map_to_list_empty. Qed.
 Lemma big_opM_insert (m : M A) i x :
   m !! i = None → big_opM (<[i:=x]> m) ≡ x ⋅ big_opM m.
 Proof. intros ?; by rewrite /big_opM map_to_list_insert. Qed.
+Lemma big_opM_delete (m : M A) i x :
+  m !! i = Some x → x ⋅ big_opM (delete i m) ≡ big_opM m.
+Proof.
+  intros. by rewrite -{2}(insert_delete m i x) // big_opM_insert ?lookup_delete.
+Qed.
 Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
 Proof.
   rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
-- 
GitLab