diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 3451684..c3b28e8 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -8,6 +8,15 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Changed
+
+* resource-algebra pin `b2c9f1f` → `0b338c9` (`scripts/fetch-siblings.sh`).
+  That commit adds `≤-+ˡ`, `≤-+ʳ`, `+-monoˡ-≤` and `max-lub` to
+  `ResourceAlgebra.Prelude`, with the same statements as the copies in
+  `OccupancyTypes.Order`. Order opens the Prelude, so the two definitions
+  clashed (`Multiple definitions of ≤-+ˡ`). The local copies are removed;
+  the proofs now use the kernel's.
+
 ==== Added
 
 * `www/` site-operations bundle (issue #53): canonical `.well-known/`
diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh
index 496b7df..fc5de29 100755
--- a/scripts/check-agda.sh
+++ b/scripts/check-agda.sh
@@ -7,8 +7,7 @@ export LC_ALL="${LC_ALL:-C.UTF-8}"
 prover="${AGDA:-agda}"
 "$prover" --version
 ra="${RESOURCE_ALGEBRA_SRC:-_build/dependencies/resource-algebra/src}"
-[ -d "$ra" ] || [ -n "${RESOURCE_ALGEBRA_SRC:-}" ] || bash scripts/fetch-siblings.sh
-if [ ! -d "$ra" ] && [ "$ra" = _build/dependencies/resource-algebra/src ]; then
+if [ -z "${RESOURCE_ALGEBRA_SRC:-}" ]; then
   bash scripts/fetch-siblings.sh
 fi
 test -d "$ra" || { echo "ERROR: resource-algebra sources not found at $ra" >&2; exit 1; }
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
index 98ac0a7..b6f8c49 100755
--- a/scripts/fetch-siblings.sh
+++ b/scripts/fetch-siblings.sh
@@ -3,7 +3,7 @@
 # Fetch the compared sibling at its pinned commit (pattern: residual-evidence-types).
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
-RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-b2c9f1f6bc7ed7cc83c7573014cdf88d49d2a881}"
+RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}"
 mkdir -p _build/dependencies
 if [ ! -d _build/dependencies/resource-algebra ]; then
   git clone --quiet https://github.com/hyperpolymath/resource-algebra.git _build/dependencies/resource-algebra
diff --git a/src/OccupancyTypes/Order.agda b/src/OccupancyTypes/Order.agda
index d6a5081..b5019fc 100644
--- a/src/OccupancyTypes/Order.agda
+++ b/src/OccupancyTypes/Order.agda
@@ -14,22 +14,9 @@ m < n = suc m ≤ n
 ≤-step z≤n     = z≤n
 ≤-step (s≤s p) = s≤s (≤-step p)
 
-≤-+ˡ : ∀ n k → k ≤ n + k
-≤-+ˡ zero    k = ≤-refl k
-≤-+ˡ (suc n) k = ≤-step (≤-+ˡ n k)
-
-≤-+ʳ : ∀ m n → m ≤ m + n
-≤-+ʳ zero    n = z≤n
-≤-+ʳ (suc m) n = s≤s (≤-+ʳ m n)
-
-+-monoˡ-≤ : ∀ {m n} k → m ≤ n → m + k ≤ n + k
-+-monoˡ-≤ k (z≤n {n}) = ≤-+ˡ n k
-+-monoˡ-≤ k (s≤s p)   = s≤s (+-monoˡ-≤ k p)
-
-max-lub : ∀ {a b c} → a ≤ c → b ≤ c → max a b ≤ c
-max-lub z≤n     q       = q
-max-lub (s≤s p) z≤n     = s≤s p
-max-lub (s≤s p) (s≤s q) = s≤s (max-lub p q)
+-- ≤-+ˡ, ≤-+ʳ, +-monoˡ-≤ and max-lub were defined here until resource-algebra
+-- 0b338c9 added the same four lemmas to its Prelude (with Instances/MinMax);
+-- they now come from there, through the open import above.
 
 <-+ʳ : ∀ m {n} → 0 < n → m < m + n
 <-+ʳ m {suc n} _ = subst (suc m ≤_) (sym (+-suc m n)) (s≤s (≤-+ʳ m n))