Move ≤-pred to Data.Nat.Properties.Base

src/Data/Fin/Base.agda

@@ -14,9 +14,9 @@ module Data.Fin.Base where
 
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
+open import Data.Nat.Properties.Core using (≤-pred)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (id; _∘_; _on_)
-import Data.Nat.Properties as ℕₚ
 open import Level using () renaming (zero to ℓ₀)
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
@@ -66,7 +66,7 @@ fromℕ (suc n) = suc (fromℕ n)
 
 fromℕ< : ∀ {m n} → m ℕ.< n → Fin n
 fromℕ< {zero}  {suc n} m≤n = zero
-fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (ℕₚ.≤-pred m≤n))
+fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (≤-pred m≤n))
 
 -- fromℕ<″ m _ = "m".
 
@@ -107,7 +107,7 @@ inject₁ (suc i) = suc (inject₁ i)
 
 inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
 inject≤ {_} {suc n} zero    le = zero
-inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (ℕₚ.≤-pred le))
+inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (≤-pred le))
 
 -- lower₁ "i" _ = "i".
 

src/Data/Nat/Properties.agda

@@ -107,8 +107,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 -- Properties of _≤_
 ------------------------------------------------------------------------
 
-≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
+open import Data.Nat.Properties.Core public
 
 ------------------------------------------------------------------------
 -- Relational properties of _≤_

src/Data/Nat/Properties/Core.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- ≤-pred definition so as to not cause dependency problems.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Properties.Core where
+
+open import Data.Nat.Base
+
+------------------------------------------------------------------------
+-- Properties of _≤_
+------------------------------------------------------------------------
+
+≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
+≤-pred (s≤s m≤n) = m≤n