diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 660d174cb9dc320deaa232442449ead0e117a297..97d711b50deb55750f2b5607113a630ef79f3afb 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -291,12 +291,17 @@ Proof.
   iSpecialize ("HÏ†" with "[% //] HP"). done.
 Qed.
 
-Lemma test_iNext_laterN_later P n : â–· â–·^n P âŠ¢ â–·^n â–· P.
+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.
+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.
+Lemma test_iNext_plus_1 P n1 n2 : â–· â–·^n1 â–·^n2 P -âˆ— â–·^n1 â–·^n2 â–· P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+Lemma test_iNext_plus_2 P n m : â–·^n â–·^m P -âˆ— â–·^(n+m) P.
+Proof. iIntros "H". iNext. done. Qed.
+Lemma test_iNext_plus_3 P Q n m k :
+  â–·^m â–·^(2 + S n + k) P -âˆ— â–·^m â–· â–·^(2 + S n) Q -âˆ— â–·^k â–· â–·^(S (S n + S m)) (P âˆ— Q).
+Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
 
 Lemma test_iEval x y : âŒœ (y + x)%nat = 1 âŒ -âˆ— âŒœ S (x + y) = 2%nat âŒ : uPred M.
 Proof.