diff --git a/program_logic/auth.v b/program_logic/auth.v
index 6f966d983b48d95b5e2f5de6768d782fa44fa8a6..58d63dcd9ae4af72eb0d869450c409692b69ad4d 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -55,6 +55,10 @@ Section auth.
 
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
+
+  Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
+  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.