From a994cbc321f78776b11d3fa9aba3f51c530764e2 Mon Sep 17 00:00:00 2001
From: Alvin Tang <alvin.tang@ist.ac.at>
Date: Thu, 16 Jul 2026 13:13:31 +0200
Subject: [PATCH] Use `Nat.repeat` for the definition of `BIBase.laterN`

---
 Iris/Iris/BI/BIBase.lean           | 3 +--
 Iris/Iris/BI/DerivedLawsLater.lean | 8 ++++++--
 Iris/Iris/Instances/Lib/FUpd.lean  | 2 +-
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean
index 48f9f37db..9a7f514bd 100644
--- a/Iris/Iris/BI/BIBase.lean
+++ b/Iris/Iris/BI/BIBase.lean
@@ -235,8 +235,7 @@ delab_rule intuitionistically
 syntax:max "▷^[" term:45 "]" term:40 : term
 
 @[rocq_alias bi_laterN]
-def laterN [BIBase PROP] (n : Nat) (P : PROP) : PROP :=
-  match n with | .zero => P | .succ n' => later <| laterN n' P
+def laterN [BIBase PROP] (n : Nat) (P : PROP) : PROP := n.repeat later P
 
 macro_rules
   | `(iprop(▷^[$n] $P))   => ``(laterN $n iprop($P))
diff --git a/Iris/Iris/BI/DerivedLawsLater.lean b/Iris/Iris/BI/DerivedLawsLater.lean
index 3bc9ff86f..bebffc268 100644
--- a/Iris/Iris/BI/DerivedLawsLater.lean
+++ b/Iris/Iris/BI/DerivedLawsLater.lean
@@ -397,7 +397,9 @@ instance laterN_persistent (n : Nat) (P : PROP) [Persistent P] :
     Persistent iprop(▷^[n] P) := by
   induction n with
   | zero => assumption
-  | succ n _ => exact later_persistent
+  | succ n _ =>
+    dsimp only [BIBase.laterN, Nat.repeat] at *
+    exact later_persistent
 
 instance instPersistentLaterIf [BI PROP] (P : PROP) [Persistent P] (p : Bool) :
     Persistent iprop(▷?p P) := by
@@ -408,7 +410,9 @@ instance laterN_absorbing (n : Nat) (P : PROP) [Absorbing P] :
     Absorbing iprop(▷^[n] P) := by
   induction n with
   | zero => assumption
-  | succ n _ => exact later_absorbing
+  | succ n _ =>
+    dsimp only [BIBase.laterN, Nat.repeat] at *
+    exact later_absorbing
 
 /-! ## LaterN as a monoid homomorphism -/
 
diff --git a/Iris/Iris/Instances/Lib/FUpd.lean b/Iris/Iris/Instances/Lib/FUpd.lean
index b150420b0..fdfeb6645 100644
--- a/Iris/Iris/Instances/Lib/FUpd.lean
+++ b/Iris/Iris/Instances/Lib/FUpd.lean
@@ -173,7 +173,7 @@ theorem lc_fupd_add_laterN (n : Nat) {E : CoPset} {P : IProp GF} :
   induction n generalizing P with
   | zero =>
     iintro _ H
-    simp [BIBase.laterN]
+    dsimp only [BIBase.laterN, Nat.repeat]
     iexact H
   | succ n IH =>
     iintro Hf Hupd