diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 78d3feebd4f2eed4641ca34c4420a39da1970f38..b2d5d2de38a0b9f582ced050c659f69cabece28f 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -392,6 +392,8 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
+Lemma except_0_laterN n P : ◇ ▷^n P ⊢ ▷^n ◇ P.
+Proof. by destruct n as [|n]; rewrite //= ?except_0_later -except_0_intro. Qed.
 Lemma except_0_into_later P : ◇ P ⊢ ▷ P.
 Proof. by rewrite -except_0_later -later_intro. Qed.
 Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.