diff --git a/algebra/gmap.v b/algebra/gmap.v
index 6a9fdeda576b02359f454f39c7c69532d1a784a6..c33b1905e3b1b90cc9cb04179c72e7955c3fa9e9 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -202,6 +202,7 @@ Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
 Lemma lookup_valid_Some m i x : ✓ m → m !! i ≡ Some x → ✓ x.
 Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
+
 Lemma insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
 Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
@@ -214,6 +215,11 @@ Qed.
 Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
 
+Lemma delete_validN n m i : ✓{n} m → ✓{n} (delete i m).
+Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.
+Lemma delete_valid m i : ✓ m → ✓ (delete i m).
+Proof. intros Hm j; destruct (decide (i = j)); by simplify_map_eq. Qed.
+
 Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m = {[ i := x ]} ⋅ m.
 Proof.
   intros Hi; apply map_eq=> j; destruct (decide (i = j)) as [->|].