diff --git a/_CoqProject b/_CoqProject
index 5539986c7fa1d95c3895df822db38d233555eb3c..bc90218fb2771f0c20f1d1a7e13999ce890575c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
 -Q theories actris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
+theories/utils/skip.v
 theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
new file mode 100644
index 0000000000000000000000000000000000000000..6d154ded31844ccfc1c04a9b37fc085edb4773b3
--- /dev/null
+++ b/theories/utils/skip.v
@@ -0,0 +1,11 @@
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Definition skipN : val :=
+  rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
+
+Lemma skipN_spec `{heapG Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
+Proof.
+  iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
+  rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
+Qed.