diff --git a/_CoqProject b/_CoqProject
index 071cd83b170d17968892d6a7426f60a2988f83df..299bf9513a454816706d582830d72483175e7751 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -116,6 +116,8 @@ theories/heap_lang/lib/clairvoyant_coin.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
+theories/heap_lang/lib/diverge.v
+theories/heap_lang/lib/arith.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/theories/heap_lang/lib/arith.v b/theories/heap_lang/lib/arith.v
new file mode 100644
index 0000000000000000000000000000000000000000..57f7c4fb313411febc8330c11e5e950fb328d4a0
--- /dev/null
+++ b/theories/heap_lang/lib/arith.v
@@ -0,0 +1,43 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(** A library defining binary [minimum] and [maximum] functions, together with
+their expected specs. These operations come up often when working manipulating
+array indices (checking for bounds). *)
+
+Definition minimum : val :=
+  λ: "m" "n", if: "m" < "n" then "m" else "n".
+
+Definition maximum : val :=
+  λ: "m" "n", if: "m" < "n" then "n" else "m".
+
+Lemma minimum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+  ▷ Φ #(m `min` n) -∗
+  WP minimum #m #n @ s;E {{ Φ }}.
+Proof.
+  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
+  - rewrite Z.min_l; [ done | by lia ].
+  - rewrite Z.min_r; [ done | by lia ].
+Qed.
+
+Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+  ▷ Φ #(m `min` n)%nat -∗
+  WP minimum #m #n @ s;E {{ Φ }}.
+Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
+
+Lemma maximum_spec `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : Z) :
+  ▷ Φ #(m `max` n) -∗
+  WP maximum #m #n @ s;E {{ Φ }}.
+Proof.
+  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
+  - rewrite Z.max_r; [ done | by lia ].
+  - rewrite Z.max_l; [ done | by lia ].
+Qed.
+
+Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val → iProp Σ) (m n : nat) :
+  ▷ Φ #(m `max` n)%nat -∗
+  WP maximum #m #n @ s;E {{ Φ }}.
+Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
diff --git a/theories/heap_lang/lib/diverge.v b/theories/heap_lang/lib/diverge.v
new file mode 100644
index 0000000000000000000000000000000000000000..38b00be2a81578ee6c20bba006c5c83465236d7a
--- /dev/null
+++ b/theories/heap_lang/lib/diverge.v
@@ -0,0 +1,27 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(** This library provides a [diverge] function that goes into an infinite loop
+when provided with an (arbitrary) argument value. This function can be used to
+let the program diverge in corner cases that one wants to omit in proofs. This
+mechanism should be used with care and communicated clearly, obviously.
+
+Note that this mechanism only works when establishing partial correctness with
+the ordinary version of weakest preconditions, and not when establishing total
+correctness using the total version of weakest preconditions.
+
+A typical application for [diverge] is insertion functions for data structures
+having a fixed capacity. In such cases, we can choose divergence instead of an
+explicit error handling when the full capacity has already been reached. *)
+
+Definition diverge : val :=
+  rec: "diverge" "v" := "diverge" "v".
+
+Lemma wp_diverge `{!heapG Σ} s E (Φ : val → iProp Σ) (v : val) :
+  WP diverge v @ s;E {{ Φ }}%I.
+Proof.
+  iLöb as "IH". wp_lam. iApply "IH".
+Qed.