diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 91fd17a56de34eba228c2bec495c94e13ec9a1c1..bfc3a73d77c557d3264f73d2dce5a9e492d10d44 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -170,6 +170,46 @@ Proof.
   iIntros "_". iPureIntro. rewrite /num_laters_per_step /=. lia.
 Qed.
 
+(** This lemma allows to get [S n] credits on a pure step,
+  when a lower bound of [n] on the number of steps taken is available. *)
+Lemma wp_pure_step_credits_lb ϕ e1 e2 s E n Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  steps_lb n -∗
+  (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }}) -∗
+  WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (Hpure Hphi) "Hlb Hwp".
+  specialize (Hpure Hphi) as [Hsafe Hdet]%nsteps_once_inv.
+  iApply wp_lift_step_fupdN.
+  { eapply (reducible_not_val _ inhabitant). by apply reducible_no_obs_reducible. }
+  iIntros (σ1 ns κ κs nt) "(Hσ & Hκ & Hsteps)".
+  iDestruct (steps_lb_valid with "Hsteps Hlb") as %?.
+  iApply fupd_mask_intro; first set_solver. iIntros "Hcl".
+  iSplitR. { iPureIntro. destruct s; eauto using reducible_no_obs_reducible. }
+  iIntros (? σ2 efs (-> & -> & -> & ->)%Hdet) "Hcred".
+  iApply step_fupdN_intro; first done. iNext. iNext.
+  iMod "Hcl" as "_".
+  iPoseProof (lc_weaken (S n) with "Hcred") as "Hcred".
+  { rewrite /num_laters_per_step /=. lia. }
+  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
+  iPoseProof (steps_lb_get with "Hsteps") as "#HlbS".
+  iModIntro. iFrame. iSplitL; last done.
+  iDestruct (steps_lb_le _ (S n) with "HlbS") as "HlbS'"; [lia|].
+  iApply ("Hwp" with "Hcred HlbS'").
+Qed.
+
+(** This just re-exports the lifting lemma when one wants to generate a single credit during a pure step. *)
+Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
+  WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (Hexec Hphi) "Hwp".
+  iApply wp_pure_step_later; done.
+Qed.
+
 (** Recursive functions: we do not use this lemmas as it is easier to use Löb
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)