From ea869f3b0818abe71f0dc8c5b68acf87cf134ceb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 Mar 2020 21:33:33 +0100
Subject: [PATCH] Add lemma `except_0_laterN`.

---
 theories/bi/derived_laws_sbi.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 78d3feebd..b2d5d2de3 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.
-- 
GitLab