diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 8576c152523bf359bddbc7bd52c32e13fade7ae6..28488c4faebc239206df1dd0783f78f600abb2df 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -86,11 +86,11 @@ Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
   match n with
   | O => P
-  | S n' => â–· sbi_laterN n' P
-  end%I.
+  | S n' => â–· â–·^n' P
+  end%I
+where "â–·^ n P" := (sbi_laterN n P) : bi_scope.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2 := {}.
-Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
 Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
 
 Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.