diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 41542e659bf6924e78271d177114d9418fd1f98a..fbb64e79ddcb3aeeb56e78657353f1675737276c 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -136,6 +136,30 @@ Proof.
   destruct 1; destruct 1; repeat f_equiv; constructor || done.
 Qed.
 
+Global Instance gmap_union_ne `{Countable K} {A : ofe} :
+  NonExpansive2 (union (A:=gmap K A)).
+Proof. intros n. apply union_with_ne. by constructor. Qed.
+Global Instance gmap_disjoint_ne `{Countable K} {A : ofe} n :
+  Proper (dist n ==> dist n ==> iff) (map_disjoint (M:=gmap K) (A:=A)).
+Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2; split;
+    intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
+Qed.
+
+Lemma gmap_union_dist_eq `{Countable K} {A : ofe} (m m1 m2 : gmap K A) n :
+  m ≡{n}≡ m1 ∪ m2 ↔ ∃ m1' m2', m = m1' ∪ m2' ∧ m1' ≡{n}≡ m1 ∧ m2' ≡{n}≡ m2.
+Proof.
+  split; last first.
+  { by intros (m1'&m2'&->&<-&<-). }
+  intros Hm.
+  exists (filter (λ '(l,_), is_Some (m1 !! l)) m),
+    (m2 ∩ m1 ∪ filter (λ '(l,_), is_Some (m2 !! l)) m).
+  split_and!; [apply map_eq|..]; intros k; move: (Hm k);
+    rewrite ?lookup_union ?lookup_intersection !map_lookup_filter;
+    case _ : (m !! k)=> [x|] /=; case _ : (m1 !! k)=> [x1|] /=;
+      case _ : (m2 !! k)=> [x2|] /=; by inversion 1.
+Qed.
+
 Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofe} (f g : K → A → M) m1 m2 n :
   m1 ≡{n}≡ m2 →
   (∀ k y1 y2,
@@ -427,6 +451,24 @@ Proof.
   - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
 Qed.
 
+Lemma gmap_op_union m1 m2 : m1 ##ₘ m2 → m1 ⋅ m2 = m1 ∪ m2.
+Proof.
+  intros Hm. apply map_eq=> k. specialize (Hm k).
+  rewrite lookup_op lookup_union. by destruct (m1 !! k), (m2 !! k).
+Qed.
+
+Lemma gmap_op_valid0_disjoint m1 m2 :
+  ✓{0} (m1 ⋅ m2) → (∀ k x, m1 !! k = Some x → Exclusive x) → m1 ##ₘ m2.
+Proof.
+  unfold Exclusive. intros Hvalid Hexcl k.
+  specialize (Hvalid k). rewrite lookup_op in Hvalid. specialize (Hexcl k).
+  destruct (m1 !! k), (m2 !! k); [|done..].
+  rewrite -Some_op Some_validN in Hvalid. naive_solver.
+Qed.
+Lemma gmap_op_valid_disjoint m1 m2 :
+  ✓ (m1 ⋅ m2) → (∀ k x, m1 !! k = Some x → Exclusive x) → m1 ##ₘ m2.
+Proof. move=> /cmra_valid_validN /(_ 0). apply gmap_op_valid0_disjoint. Qed.
+
 Lemma dom_op m1 m2 : dom (m1 ⋅ m2) = dom m1 ∪ dom m2.
 Proof.
   apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index 6059dd538ecde7248185b9d5dd65e7a0b18a7212..c33e5b8fd6f81c01cd54541ee506ae0801e6e8a9 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -30,6 +30,10 @@ Section upred.
 
     Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
     Proof. by uPred.unseal. Qed.
+
+    Lemma gmap_union_equiv_eqI m m1 m2 :
+      m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
+    Proof. uPred.unseal; split=> n x _. apply gmap_union_dist_eq. Qed.
   End gmap_ofe.
 
   Section gmap_cmra.