diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index aa19988e144d0d79306ac1cda20e5f8c426649cd..6ebf62a342bd1c487c28d59bfe00a93720151c83 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -198,6 +198,10 @@ Section lemmas.
     ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 = m2.
   Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
 
+  Lemma gmap_view_auth_dfrac_validN m n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
+  Proof.
+    rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
+  Qed.
   Lemma gmap_view_auth_dfrac_valid m dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
   Proof.
     rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.