diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index e4d59e7830..b7550218a7 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -8,17 +8,18 @@
 
 module Data.Nat.InfinitelyOften where
 
-open import Effect.Monad using (RawMonad)
-open import Level using (Level; 0ℓ)
 open import Data.Nat.Base using (ℕ; _≤_; _⊔_; _+_; suc; zero; s≤s)
 open import Data.Nat.Properties
 open import Data.Product.Base as Prod hiding (map)
 open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
+open import Effect.Monad using (RawMonad)
 open import Function.Base using (_∘_; id)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 open RawMonad (¬¬-Monad {a = 0ℓ})