diff --git a/algebra/auth.v b/algebra/auth.v
index 45488923b38b3f830510f9639ae0707e43a2d013..4e33a44a74cbd2d3ce0863d0b95a6f98ba84e780 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -162,6 +162,9 @@ Qed.
 Canonical Structure authUR :=
   UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
+Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
+Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
+
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
   x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 58d63dcd9ae4af72eb0d869450c409692b69ad4d..9fd82aa0723fecfe6cfa3ed40b224b8bf45669ff 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -59,6 +59,10 @@ Section auth.
   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.
 
+  Global Instance auth_own_persistent γ a :
+    Persistent a → PersistentP (auth_own γ a).
+  Proof. rewrite /auth_own. apply _. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.