diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 8c3f670a6b685de341a5c060cc414f0e48eb022b..184e3ddcb9ea04229c0b36a893692553bfc1bd83 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -67,8 +67,8 @@ Section mono_nat.
     unseal. iIntros "H1 H2". Typeclasses Transparent mono_nat_auth.
     iDestruct "H1" as "[H1 H1']". (* this gets annoying because mono_nat_auth = ● _ ⋅ ◯ _ *)
     iDestruct "H2" as "[H2 H2']".
-    iDestruct (own_valid_op with "H1 H2") as "[H #H']".
-    iDestruct "H'" as "[% %]". case: H0 => ->. eauto.
+    iCombineOwn "H1 H2" as "[H [%Hq %Hnm]]".
+    case: Hnm => ->. eauto.
   Qed.
   Lemma mono_nat_auth_own_exclusive γ n1 n2 :
     mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.