diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 004892b1c9d31de207170247cfdc02853f3677c0..d3ff12d81d6622b48e7e5a107fbfd1e62512dab8 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -91,10 +91,6 @@ Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
-(** Iterated later *)
-Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n sbi_later P.
-Proof. induction n; f_equal/=; auto. Qed.
-
 (** Consistency/soundness statement *)
 Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof. rewrite laterN_iter. apply soundness_iter. Qed.
diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 842fcdaa12403c51136789be2435a69e23b7fffd..e1e93317e3141335110f5f980bfefd8ee4254eb2 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -247,6 +247,9 @@ Proof. induction n1; f_equiv/=; auto. Qed.
 Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
 Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
 
+Lemma laterN_iter n P : (â–·^n P)%I = Nat.iter n sbi_later P.
+Proof. induction n; f_equal/=; auto. Qed.
+
 Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q.
 Proof. induction n; simpl; auto. Qed.
 Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@sbi_laterN PROP n).