diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index a3cad0ca9ab8a5cc89b0757710ddcfb7a1e18deb..caaabaec9e0b9e4fd7088ed32ce6b69ae86df9a6 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -278,6 +278,13 @@ Proof.
iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
+Lemma test_iNext_laterN_later P n : ▷ ▷^n P ⊢ ▷^n ▷ P.
+Proof. iIntros "H". iNext. by iNext. Qed.
+Lemma test_iNext_later_laterN P n : ▷^n ▷ P ⊢ ▷ ▷^n P.
+Proof. iIntros "H". iNext. by iNext. Qed.
+Lemma test_iNext_laterN_laterN P n1 n2 : ▷ ▷^n1 ▷^n2 P ⊢ ▷^n1 ▷^n2 ▷ P.
+Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+
(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *)
(*