diff --git a/eratosthenes.agda-lib b/eratosthenes.agda-lib
index a835a3c..794ebfc 100644
--- a/eratosthenes.agda-lib
+++ b/eratosthenes.agda-lib
@@ -1,3 +1,3 @@
 name: eratosthenes
 include: src
-depend: standard-library-2.1
+depend: standard-library-2.4
diff --git a/src/Eratosthenes.agda b/src/Eratosthenes.agda
index f8c48c7..3f578de 100644
--- a/src/Eratosthenes.agda
+++ b/src/Eratosthenes.agda
@@ -10,7 +10,7 @@ module Eratosthenes where
 
 open import Data.Nat.Base
 open import Data.Nat.Induction using (<-wellFounded-fast)
-open import Data.Nat.Properties hiding (≤-total; ≤-isTotalOrder; ≤-totalOrder)
+open import Data.Nat.Properties
 open import Data.List.Base hiding (upTo)
 open import Data.Product.Base
 open import Data.Sum.Base using (inj₁; inj₂)
@@ -27,24 +27,6 @@ open import Relation.Nullary.Decidable
 -- Reimplementations of a couple of things from stdlib because
 -- their existing definitions at time of writing are slow
 
--- ≤-total is currently defined in stdlib using unary arithmetic. This makes it
--- terrible to use as a conditional. Our heap implementation is generic over a
--- total order, so we redefine this and the bundle we care ultimately care
--- about.
-≤-total : Total _≤_
-≤-total m n with m ≤? n
-... | yes m≤n = inj₁ m≤n
-... | no m≰n = inj₂ (≰⇒≥ m≰n)
-
-≤-isTotalOrder : IsTotalOrder _≡_ _≤_
-≤-isTotalOrder = record
-  { isPartialOrder = ≤-isPartialOrder
-  ; total = ≤-total
-  }
-
-≤-totalOrder : TotalOrder _ _ _
-≤-totalOrder = record { isTotalOrder = ≤-isTotalOrder }
-
 -- upTo in stdlib creates larger and larger closures. This causes some slowdown.
 -- We implement it in a tail recursive manner instead.
 upFromThen : ℕ → ℕ → List ℕ