diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 8da81d331febc50eaef975ad049093d221a4197c..d60d9a75eec8975d7ca5527f266c30b8c23c6bd6 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -850,6 +850,12 @@ Proof.
   - rewrite comm persistently_absorbing. done.
 Qed.
 
+Lemma persistently_alt_fixpoint' P :
+  <pers> P ⊣⊢ <affine> P ∗ <pers> P.
+Proof.
+  rewrite -{1}persistently_affinely {1}persistently_alt_fixpoint persistently_affinely //.
+Qed.
+
 Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.