diff --git a/CHANGELOG.md b/CHANGELOG.md
index c8c5364464..905e469c2d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -518,6 +518,10 @@ Deprecated modules
   Relation.Binary.Properties.MeetSemilattice.agda         ↦ Relation.Binary.Lattice.Properties.MeetSemilattice.agda
   ```
 
+### Deprecation of `Data.Nat.Properties.Core`
+
+* The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties`
+
 Deprecated names
 ----------------
 
@@ -1003,6 +1007,8 @@ Other minor changes
   combine-surjective : ∀ x → ∃₂ λ y z → combine y z ≡ x
 
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
+
+  i<1+i              : i < suc i
   ```
 
 * Added new functions in `Data.Integer.Base`:
@@ -1065,6 +1071,16 @@ Other minor changes
   ∷ʳ-++ : xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
   ```
 
+* Added new patterns and definitions to `Data.Nat.Base`:
+  ```agda
+  pattern z<s {n}         = s≤s (z≤n {n})
+  pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+
+  pattern <′-base          = ≤′-refl
+  pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+  ```
+
+
 * Added new definitions and proofs to `Data.Nat.Primality`:
   ```agda
   Composite        : ℕ → Set
@@ -1087,6 +1103,17 @@ Other minor changes
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
+  ≤-pred        : suc m ≤ suc n → m ≤ n
+  s<s-injective : ∀ {p q : m < n} → s<s p ≡ s<s q → p ≡ q
+  <-pred        : suc m < suc n → m < n
+  <-step        : m < n → m < 1 + n
+  m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
+
+  z<′s : zero <′ suc n
+  s<′s : m <′ n → suc m <′ suc n
+  <⇒<′ : m < n → m <′ n
+  <′⇒< : m <′ n → m < n
+
   1≤n!    : 1 ≤ n !
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 9fce61af4b..3a39a2f992 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -13,8 +13,7 @@
 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.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
@@ -67,8 +66,8 @@ fromℕ (suc n) = suc (fromℕ n)
 -- fromℕ< {m} _ = "m".
 
 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ℕ< {zero}  {suc n} z<s = zero
+fromℕ< {suc m} {suc n} (s<s m<n) = suc (fromℕ< m<n)
 
 -- fromℕ<″ m _ = "m".
 
@@ -112,8 +111,8 @@ inject₁ zero    = zero
 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} zero    _        = zero
+inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 
 -- lower₁ "i" _ = "i".
 
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index 8945f5fbd1..688ff8327e 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -8,7 +8,7 @@
 
 open import Data.Fin.Base
 open import Data.Fin.Properties
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; _∸_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_)
 import Data.Nat.Induction as ℕ
 import Data.Nat.Properties as ℕ
 open import Induction
@@ -46,15 +46,15 @@ open WF public using (Acc; acc)
   induct : ∀ {i} → Acc _<_ i → P i
   induct {zero}  _         = P₀
   induct {suc i} (acc rec) = Pᵢ⇒Pᵢ₊₁ i (induct (rec (inject₁ i) i<i+1))
-    where i<i+1 = s≤s (ℕ.≤-reflexive (toℕ-inject₁ i))
+    where i<i+1 = ℕ<⇒inject₁< (i<1+i i)
 
 ------------------------------------------------------------------------
 -- Induction over _>_
 
 private
   acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
-  acc-map {n} (acc rs) = acc (λ y y>x →
-    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y))))
+  acc-map {n} (acc rs) = acc λ y y>x →
+    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -69,7 +69,7 @@ private
   induct {i} (acc rec) with n ℕ.≟ toℕ i
   ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
-    where Pᵢ₊₁ = induct (rec _ (s≤s (ℕ.≤-reflexive (sym (toℕ-lower₁ i n≢i)))))
+    where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Induction over _≺_
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index fed4a2ae61..4d80c7bcab 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -17,7 +17,7 @@ open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
@@ -135,17 +135,20 @@ toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 ↑ʳ-injective zero i i refl = refl
 ↑ʳ-injective (suc n) i j eq = ↑ʳ-injective n i j (suc-injective eq)
 
-toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ.< n
-toℕ<n zero    = s≤s z≤n
-toℕ<n (suc i) = s≤s (toℕ<n i)
-
-toℕ≤n : ∀ {n} → (i : Fin n) → toℕ i ℕ.≤ n
-toℕ≤n = ℕₚ.<⇒≤ ∘ toℕ<n
+------------------------------------------------------------------------
+-- toℕ and the ordering relations
+------------------------------------------------------------------------
 
 toℕ≤pred[n] : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n] zero                 = z≤n
 toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 
+toℕ≤n : ∀ {n} → (i : Fin n) → toℕ i ℕ.≤ n
+toℕ≤n {suc n} i = ℕₚ.≤-step (toℕ≤pred[n] i)
+
+toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ.< n
+toℕ<n {suc n} i = s≤s (toℕ≤pred[n] i)
+
 -- A simpler implementation of toℕ≤pred[n],
 -- however, with a different reduction behavior.
 -- If no one needs the reduction behavior of toℕ≤pred[n],
@@ -153,21 +156,19 @@ toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 toℕ≤pred[n]′ : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
 toℕ≤pred[n]′ i = ℕₚ.<⇒≤pred (toℕ<n i)
 
+-- In view of the defintions now in Data.Fin.Base,
+-- are these four lemmas not all the identity function?
 toℕ-mono-< : ∀ {n} {i j : Fin n} → i < j → toℕ i ℕ.< toℕ j
-toℕ-mono-< {i = 0F}    {suc j}       (s≤s z≤n)       = s≤s z≤n
-toℕ-mono-< {i = suc i} {suc (suc j)} (s≤s (s≤s i<j)) = s≤s (toℕ-mono-< (s≤s i<j))
+toℕ-mono-< i<j = i<j
 
 toℕ-mono-≤ : ∀ {n} {i j : Fin n} → i ≤ j → toℕ i ℕ.≤ toℕ j
-toℕ-mono-≤ {i = 0F} {j} z≤n = z≤n
-toℕ-mono-≤ {i = suc i} {suc j} (s≤s i≤j) = s≤s (toℕ-mono-≤ i≤j)
+toℕ-mono-≤ i≤j = i≤j
 
 toℕ-cancel-≤ : ∀ {n} {i j : Fin n} → toℕ i ℕ.≤ toℕ j → i ≤ j
-toℕ-cancel-≤ {i = 0F} {j} z≤n = z≤n
-toℕ-cancel-≤ {i = suc i} {suc j} (s≤s i≤j) = s≤s (toℕ-cancel-≤ i≤j)
+toℕ-cancel-≤ i≤j = i≤j
 
 toℕ-cancel-< : ∀ {n} {i j : Fin n} → toℕ i ℕ.< toℕ j → i < j
-toℕ-cancel-< {i = 0F} {suc j} (s≤s z≤n) = s≤s z≤n
-toℕ-cancel-< {i = suc i} {suc (suc j)} (s≤s (s≤s i<j)) = s≤s (toℕ-cancel-< (s≤s i<j))
+toℕ-cancel-< i<j = i<j
 
 ------------------------------------------------------------------------
 -- fromℕ
@@ -182,19 +183,19 @@ fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
 ≤fromℕ : ∀ {n} → (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
-≤fromℕ {n} i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ n)) (ℕₚ.≤-pred (toℕ<n i))
+≤fromℕ {n} i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ n)) (toℕ≤pred[n] i)
 
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
 fromℕ<-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ.< m) → fromℕ< i<m ≡ i
-fromℕ<-toℕ zero    (s≤s z≤n)       = refl
-fromℕ<-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ<-toℕ i (s≤s m≤n))
+fromℕ<-toℕ zero    z<s       = refl
+fromℕ<-toℕ (suc i) (s<s m<n) = cong suc (fromℕ<-toℕ i m<n)
 
 toℕ-fromℕ< : ∀ {m n} (m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< (s≤s z≤n)       = refl
-toℕ-fromℕ< (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ< (s≤s m<n))
+toℕ-fromℕ< z<s               = refl
+toℕ-fromℕ< (s<s m<n@(s≤s _)) = cong suc (toℕ-fromℕ< m<n)
 
 -- fromℕ is a special case of fromℕ<.
 fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
@@ -205,18 +206,18 @@ fromℕ<-cong : ∀ m n {o} → m ≡ n →
               (m<o : m ℕ.< o) →
               (n<o : n ℕ.< o) →
               fromℕ< m<o ≡ fromℕ< n<o
-fromℕ<-cong 0       0       r (s≤s z≤n)     (s≤s z≤n)     = refl
-fromℕ<-cong (suc _) (suc _) r (s≤s (s≤s p)) (s≤s (s≤s q))
-  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) (s≤s p) (s≤s q))
+fromℕ<-cong 0       0       r z<s       z<s  = refl
+fromℕ<-cong (suc _) (suc _) r (s<s m<n) (s<s n<o)
+  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) m<n n<o)
 
 fromℕ<-injective : ∀ m n {o} →
                    (m<o : m ℕ.< o) →
                    (n<o : n ℕ.< o) →
                    fromℕ< m<o ≡ fromℕ< n<o →
                    m ≡ n
-fromℕ<-injective 0 0 (s≤s z≤n) (s≤s z≤n) r = refl
-fromℕ<-injective (suc _) (suc _) (s≤s (s≤s p)) (s≤s (s≤s q)) r
-  = cong suc (fromℕ<-injective _ _ (s≤s p) (s≤s q) (suc-injective r))
+fromℕ<-injective 0       0       z<s               z<s r = refl
+fromℕ<-injective (suc _) (suc _) (s<s m<n@(s≤s _)) (s<s n<o@(s≤s _)) r
+  = cong suc (fromℕ<-injective _ _ m<n n<o (suc-injective r))
 
 ------------------------------------------------------------------------
 -- fromℕ<″
@@ -224,9 +225,9 @@ fromℕ<-injective (suc _) (suc _) (s≤s (s≤s p)) (s≤s (s≤s q)) r
 
 fromℕ<≡fromℕ<″ : ∀ {m n} (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-fromℕ<≡fromℕ<″ (s≤s z≤n)       (ℕ.less-than-or-equal refl) = refl
-fromℕ<≡fromℕ<″ (s≤s (s≤s m<n)) (ℕ.less-than-or-equal refl) =
-  cong suc (fromℕ<≡fromℕ<″ (s≤s m<n) (ℕ.less-than-or-equal refl))
+fromℕ<≡fromℕ<″ z<s               (ℕ.less-than-or-equal refl) = refl
+fromℕ<≡fromℕ<″ (s<s m<n@(s≤s _)) (ℕ.less-than-or-equal refl) =
+  cong suc (fromℕ<≡fromℕ<″ m<n (ℕ.less-than-or-equal refl))
 
 toℕ-fromℕ<″ : ∀ {m n} (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<n = begin
@@ -341,12 +342,12 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 <-trans = ℕₚ.<-trans
 
 <-cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
-<-cmp zero    zero    = tri≈ (λ())     refl  (λ())
-<-cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
-<-cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
+<-cmp zero    zero    = tri≈ (λ()) refl  (λ())
+<-cmp zero    (suc j) = tri< z<s   (λ()) (λ())
+<-cmp (suc i) zero    = tri> (λ()) (λ()) z<s
 <-cmp (suc i) (suc j) with <-cmp i j
-... | tri< i<j i≢j j≮i = tri< (s≤s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
-... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s≤s j<i)
+... | tri< i<j i≢j j≮i = tri< (s<s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
+... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s<s j<i)
 ... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
 
 <-respˡ-≡ : ∀ {m n} → (_<_ {m} {n}) Respectsˡ _≡_
@@ -395,14 +396,17 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 ------------------------------------------------------------------------
 -- Other properties
 
+i<1+i : ∀ {n} (i : Fin n) → i < suc i
+i<1+i = ℕₚ.n<1+n ∘ toℕ
+
 <⇒≢ : ∀ {n} {i j : Fin n} → i < j → i ≢ j
 <⇒≢ i<i refl = ℕₚ.n≮n _ i<i
 
 ≤∧≢⇒< : ∀ {n} {i j : Fin n} → i ≤ j → i ≢ j → i < j
 ≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
-≤∧≢⇒< {i = zero}  {suc j} _         _       = s≤s z≤n
+≤∧≢⇒< {i = zero}  {suc j} _         _       = z<s
 ≤∧≢⇒< {i = suc i} {suc j} (s≤s i≤j) 1+i≢1+j =
-  s≤s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))
+  s<s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))
 
 ------------------------------------------------------------------------
 -- inject
@@ -436,11 +440,11 @@ inject₁ℕ≤ : ∀ {n} → (i : Fin n) → toℕ (inject₁ i) ℕ.≤ n
 inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 
 ≤̄⇒inject₁< : ∀ {n} → {i j : Fin n} → j ≤ i → inject₁ j < suc i
-≤̄⇒inject₁< {i = i} {j} p = subst (ℕ._< toℕ (suc i)) (sym (toℕ-inject₁ j)) (s≤s p)
+≤̄⇒inject₁< {i = i} {j} p = subst (ℕ._< toℕ (suc i)) (sym (toℕ-inject₁ j)) (s<s p)
 
 ℕ<⇒inject₁< : ∀ {n} → {i : Fin (ℕ.suc n)} → {j : Fin n} →
               toℕ j ℕ.< toℕ i → inject₁ j < i
-ℕ<⇒inject₁< {i = suc i} (s≤s p) = ≤̄⇒inject₁< p
+ℕ<⇒inject₁< {i = suc i} (s≤s j≤i) = ≤̄⇒inject₁< j≤i
 
 ------------------------------------------------------------------------
 -- lower₁
@@ -497,21 +501,21 @@ inject₁≡⇒lower₁≡ ≢p ≡p = inject₁-injective (trans (inject₁-low
 -- inject≤
 ------------------------------------------------------------------------
 
-toℕ-inject≤ : ∀ {m n} (i : Fin m) (le : m ℕ.≤ n) →
-                toℕ (inject≤ i le) ≡ toℕ i
-toℕ-inject≤ {_} {suc n} zero    _  = refl
-toℕ-inject≤ {_} {suc n} (suc i) le = cong suc (toℕ-inject≤ i (ℕₚ.≤-pred le))
+toℕ-inject≤ : ∀ {m n} (i : Fin m) (m≤n : m ℕ.≤ n) →
+                toℕ (inject≤ i m≤n) ≡ toℕ i
+toℕ-inject≤ {_} {suc n} zero    _         = refl
+toℕ-inject≤ {_} {suc n} (suc i) (s≤s m≤n) = cong suc (toℕ-inject≤ i m≤n)
 
 inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
 inject≤-refl {suc n} zero    _   = refl
-inject≤-refl {suc n} (suc i) n≤n = cong suc (inject≤-refl i (ℕₚ.≤-pred n≤n))
+inject≤-refl {suc n} (suc i) (s≤s n≤n) = cong suc (inject≤-refl i n≤n)
 
 inject≤-idempotent : ∀ {m n k} (i : Fin m)
                      (m≤n : m ℕ.≤ n) (n≤k : n ℕ.≤ k) (m≤k : m ℕ.≤ k) →
                      inject≤ (inject≤ i m≤n) n≤k ≡ inject≤ i m≤k
 inject≤-idempotent {_} {suc n} {suc k} zero    _   _   _ = refl
-inject≤-idempotent {_} {suc n} {suc k} (suc i) m≤n n≤k _ =
-  cong suc (inject≤-idempotent i (ℕₚ.≤-pred m≤n) (ℕₚ.≤-pred n≤k) _)
+inject≤-idempotent {_} {suc n} {suc k} (suc i) (s≤s m≤n) (s≤s n≤k) (s≤s m≤k) =
+  cong suc (inject≤-idempotent i m≤n n≤k m≤k)
 
 inject≤-injective : ∀ {n m} (n≤m n≤m′ : n ℕ.≤ m) x y → inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
 inject≤-injective (s≤s p) (s≤s q) zero zero eq = refl
@@ -522,7 +526,7 @@ inject≤-injective (s≤s p) (s≤s q) (suc x) (suc y) eq =
 -- pred
 ------------------------------------------------------------------------
 
-pred< : ∀ {n} → (i : Fin (ℕ.suc n)) → i ≢ zero → pred i < i
+pred< : ∀ {n} → (i : Fin (suc n)) → i ≢ zero → pred i < i
 pred< zero p = contradiction refl p
 pred< (suc i) p = ≤̄⇒inject₁< ℕₚ.≤-refl
 
@@ -557,8 +561,8 @@ join-splitAt (suc m) n (suc i) = begin
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
 splitAt-< : ∀ m {n} i → (i<m : toℕ i ℕ.< m) → splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
-splitAt-< (suc m) zero    _         = refl
-splitAt-< (suc m) (suc i) (s≤s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
+splitAt-< (suc m) zero    z<s               = refl
+splitAt-< (suc m) (suc i) (s<s i<m) = cong (Sum.map suc id) (splitAt-< m i i<m)
 
 -- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
 
@@ -636,7 +640,7 @@ combine-injective i j k l combine[i,j]≡combine[k,l] =
   lemma₂ i j k l combine[i,j]≡combine[k,l] , lemma₃ i j k l combine[i,j]≡combine[k,l]
   where
     lemma₁ : ∀ {n m} (i : Fin n) (j : Fin m) (k : Fin n) (l : Fin m) → i < k → combine i j < combine k l
-    lemma₁ {n} {m} i j k l i<k = toℕ-cancel-< (begin-strict
+    lemma₁ {n} {m} i j k l i<k = begin-strict
       toℕ (combine i j)      ≡⟨ toℕ-combine i j ⟩
       m ℕ.* toℕ i ℕ.+ toℕ j  <⟨ ℕₚ.+-monoʳ-< (m ℕ.* toℕ i) (toℕ<n j) ⟩
       m ℕ.* toℕ i ℕ.+ m      ≡⟨ ℕₚ.+-comm _ m ⟩
@@ -645,7 +649,7 @@ combine-injective i j k l combine[i,j]≡combine[k,l] =
       m ℕ.* suc (toℕ i)      ≤⟨ ℕₚ.*-monoʳ-≤ m (toℕ-mono-< i<k) ⟩
       m ℕ.* toℕ k            ≤⟨ ℕₚ.m≤m+n (m ℕ.* toℕ k) (toℕ l) ⟩
       m ℕ.* toℕ k ℕ.+ toℕ l  ≡˘⟨ toℕ-combine k l ⟩
-      toℕ (combine k l)      ∎)
+      toℕ (combine k l)      ∎
       where
         open ℕₚ.≤-Reasoning
         open +-*-Solver
@@ -760,8 +764,8 @@ lift-injective f inj (suc k) {suc i} {suc y} eq = cong suc (lift-injective f inj
 ------------------------------------------------------------------------
 
 <⇒≤pred : ∀ {n} {i j : Fin n} → j < i → j ≤ pred i
-<⇒≤pred {i = suc i} {zero}  j<i       = z≤n
-<⇒≤pred {i = suc i} {suc j} (s≤s j<i) =
+<⇒≤pred {i = suc i} {zero}  z<s       = z≤n
+<⇒≤pred {i = suc i} {suc j} (s<s j<i) =
   subst (_ ℕ.≤_) (sym (toℕ-inject₁ i)) j<i
 
 ------------------------------------------------------------------------
@@ -942,10 +946,10 @@ private
 
 pigeonhole : ∀ {m n} → m ℕ.< n → (f : Fin n → Fin m) →
              ∃₂ λ i j → i ≢ j × f i ≡ f j
-pigeonhole (s≤s z≤n)       f = contradiction (f zero) λ()
-pigeonhole (s≤s (s≤s m≤n)) f with any? (λ k → f zero ≟ f (suc k))
+pigeonhole z<s       f = contradiction (f zero) λ()
+pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , (λ()) , f₀≡fⱼ
-... | no  f₀≢fₖ with pigeonhole (s≤s m≤n) (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+... | no  f₀≢fₖ with pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
 ...   | (i , j , i≢j , fᵢ≡fⱼ) =
   suc i , suc j , i≢j ∘ suc-injective ,
   punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
@@ -996,7 +1000,7 @@ opposite-involutive : ∀ {n} → Involutive {A = Fin n} _≡_ opposite
 opposite-involutive {suc n} i = toℕ-injective (begin
   toℕ (opposite (opposite i)) ≡⟨ opposite-prop (opposite i) ⟩
   n ∸ (toℕ (opposite i))     ≡⟨ cong (n ∸_) (opposite-prop i) ⟩
-  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (ℕₚ.≤-pred (toℕ<n i)) ⟩
+  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (toℕ≤pred[n] i) ⟩
   toℕ i                     ∎)
   where open ≡-Reasoning
 
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 828f78fbd5..259bb0979b 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -55,6 +55,14 @@ data _≤_ : Rel ℕ 0ℓ where
 _<_ : Rel ℕ 0ℓ
 m < n = suc m ≤ n
 
+-- Smart constructors of _<_
+
+pattern z<s {n}         = s≤s (z≤n {n})
+pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+
+------------------------------------------------------------------------
+-- other ordering relations
+
 _≥_ : Rel ℕ 0ℓ
 m ≥ n = n ≤ m
 
@@ -101,7 +109,7 @@ instance
 ≢-nonZero {suc n} n≢0 = _
 
 >-nonZero : ∀ {n} → n > 0 → NonZero n
->-nonZero (s≤s 0<n) = _
+>-nonZero z<s = _
 
 -- Destructors
 
@@ -109,7 +117,7 @@ instance
 ≢-nonZero⁻¹ (suc n) ()
 
 >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
->-nonZero⁻¹ (suc n) = s≤s z≤n
+>-nonZero⁻¹ (suc n) = z<s
 
 ------------------------------------------------------------------------
 -- Arithmetic
@@ -205,6 +213,11 @@ data _≤′_ (m : ℕ) : ℕ → Set where
 _<′_ : Rel ℕ 0ℓ
 m <′ n = suc m ≤′ n
 
+-- Smart constructors of _<′_
+
+pattern <′-base          = ≤′-refl
+pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+
 _≥′_ : Rel ℕ 0ℓ
 m ≥′ n = n ≤′ m
 
diff --git a/src/Data/Nat/Induction.agda b/src/Data/Nat/Induction.agda
index 55e699bb43..f564b79268 100644
--- a/src/Data/Nat/Induction.agda
+++ b/src/Data/Nat/Induction.agda
@@ -10,7 +10,7 @@ module Data.Nat.Induction where
 
 open import Function
 open import Data.Nat.Base
-open import Data.Nat.Properties using (≤⇒≤′; n<1+n)
+open import Data.Nat.Properties using (<⇒<′)
 open import Data.Product
 open import Data.Unit.Polymorphic
 open import Induction
@@ -63,14 +63,15 @@ cRec = build cRecBuilder
 <′-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
 <′-Rec = WfRec _<′_
 
-mutual
+-- mutual definition
 
-  <′-wellFounded : WellFounded _<′_
-  <′-wellFounded n = acc (<′-wellFounded′ n)
+<′-wellFounded : WellFounded _<′_
+<′-wellFounded′ : ∀ n → <′-Rec (Acc _<′_) n
 
-  <′-wellFounded′ : ∀ n → <′-Rec (Acc _<′_) n
-  <′-wellFounded′ (suc n) .n ≤′-refl       = <′-wellFounded n
-  <′-wellFounded′ (suc n)  m (≤′-step m<n) = <′-wellFounded′ n m m<n
+<′-wellFounded n = acc (<′-wellFounded′ n)
+
+<′-wellFounded′ (suc n) n <′-base       = <′-wellFounded n
+<′-wellFounded′ (suc n) m (<′-step m<n) = <′-wellFounded′ n m m<n
 
 module _ {ℓ} where
   open WF.All <′-wellFounded ℓ public
@@ -86,7 +87,7 @@ module _ {ℓ} where
 <-Rec = WfRec _<_
 
 <-wellFounded : WellFounded _<_
-<-wellFounded = Subrelation.wellFounded ≤⇒≤′ <′-wellFounded
+<-wellFounded = Subrelation.wellFounded <⇒<′ <′-wellFounded
 
 -- A version of `<-wellFounded` that cheats by skipping building
 -- the first billion proofs. Use this when you require the function
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index c8a925945a..ae1fd5809f 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -111,12 +111,12 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ------------------------------------------------------------------------
 
 <ᵇ⇒< : ∀ m n → T (m <ᵇ n) → m < n
-<ᵇ⇒< zero    (suc n) m<n = s≤s z≤n
-<ᵇ⇒< (suc m) (suc n) m<n = s≤s (<ᵇ⇒< m n m<n)
+<ᵇ⇒< zero    (suc n) m<n = z<s
+<ᵇ⇒< (suc m) (suc n) m<n = s<s (<ᵇ⇒< m n m<n)
 
 <⇒<ᵇ : ∀ {m n} → m < n → T (m <ᵇ n)
-<⇒<ᵇ (s≤s z≤n)       = tt
-<⇒<ᵇ (s≤s (s≤s m<n)) = <⇒<ᵇ (s≤s m<n)
+<⇒<ᵇ z<s               = tt
+<⇒<ᵇ (s<s m<n@(s≤s _)) = <⇒<ᵇ m<n
 
 <ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
 <ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ
@@ -140,8 +140,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 -- Properties of _≤_
 ------------------------------------------------------------------------
 
-open import Data.Nat.Properties.Core public
-
 ------------------------------------------------------------------------
 -- Relational properties of _≤_
 
@@ -254,6 +252,9 @@ _≥?_ = flip _≤?_
 s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
+≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
+≤-pred (s≤s m≤n) = m≤n
+
 ≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
 ≤-step z≤n       = z≤n
 ≤-step (s≤s m≤n) = s≤s (≤-step m≤n)
@@ -262,7 +263,7 @@ n≤1+n : ∀ n → n ≤ 1 + n
 n≤1+n _ = ≤-step ≤-refl
 
 1+n≰n : ∀ {n} → 1 + n ≰ n
-1+n≰n (s≤s le) = 1+n≰n le
+1+n≰n (s≤s 1+n≤n) = 1+n≰n 1+n≤n
 
 n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
 n≤0⇒n≡0 z≤n = refl
@@ -274,7 +275,8 @@ n≤0⇒n≡0 z≤n = refl
 -- Relationships between the various relations
 
 <⇒≤ : _<_ ⇒ _≤_
-<⇒≤ (s≤s m≤n) = ≤-step m≤n
+<⇒≤ z<s               = z≤n
+<⇒≤ (s<s m<n@(s≤s _)) = s≤s (<⇒≤ m<n)
 
 <⇒≢ : _<_ ⇒ _≢_
 <⇒≢ m<n refl = 1+n≰n m<n
@@ -296,22 +298,22 @@ n≤0⇒n≡0 z≤n = refl
 
 ≰⇒> : _≰_ ⇒ _>_
 ≰⇒> {zero}          z≰n = contradiction z≤n z≰n
-≰⇒> {suc m} {zero}  _   = s≤s z≤n
-≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))
+≰⇒> {suc m} {zero}  _   = z<s
+≰⇒> {suc m} {suc n} m≰n = s<s (≰⇒> (m≰n ∘ s≤s))
 
 ≰⇒≥ : _≰_ ⇒ _≥_
 ≰⇒≥ = <⇒≤ ∘ ≰⇒>
 
 ≮⇒≥ : _≮_ ⇒ _≥_
 ≮⇒≥ {_}     {zero}  _       = z≤n
-≮⇒≥ {zero}  {suc j} 1≮j+1   = contradiction (s≤s z≤n) 1≮j+1
-≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s≤s))
+≮⇒≥ {zero}  {suc j} 1≮j+1   = contradiction z<s 1≮j+1
+≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s<s))
 
 ≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
 ≤∧≢⇒< {_} {zero}  z≤n       m≢n     = contradiction refl m≢n
-≤∧≢⇒< {_} {suc n} z≤n       m≢n     = s≤s z≤n
+≤∧≢⇒< {_} {suc n} z≤n       m≢n     = z<s
 ≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
-  s≤s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))
+  s<s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))
 
 ≤∧≮⇒≡ : ∀ {m n} → m ≤ n → m ≮ n → m ≡ n
 ≤∧≮⇒≡ m≤n m≮n = ≤-antisym m≤n (≮⇒≥ m≮n)
@@ -334,10 +336,10 @@ n≤0⇒n≡0 z≤n = refl
 -- Relational properties of _<_
 
 <-irrefl : Irreflexive _≡_ _<_
-<-irrefl refl (s≤s n<n) = <-irrefl refl n<n
+<-irrefl refl (s<s n<n) = <-irrefl refl n<n
 
 <-asym : Asymmetric _<_
-<-asym (s≤s n<m) (s≤s m<n) = <-asym n<m m<n
+<-asym (s<s n<m) (s<s m<n) = <-asym n<m m<n
 
 <-trans : Transitive _<_
 <-trans (s≤s i≤j) (s≤s j<k) = s≤s (≤-trans i≤j (≤-trans (n≤1+n _) j<k))
@@ -405,6 +407,16 @@ _>?_ = flip _<?_
 ------------------------------------------------------------------------
 -- Other properties of _<_
 
+s<s-injective : ∀ {m n} {p q : m < n} → s<s p ≡ s<s q → p ≡ q
+s<s-injective refl = refl
+
+<-pred : ∀ {m n} → suc m < suc n → m < n
+<-pred (s<s m<n) = m<n
+
+<-step : ∀ {m n} → m < n → m < 1 + n
+<-step z<s               = z<s
+<-step (s<s m<n@(s≤s _)) = s<s (<-step m<n)
+
 n≮0 : ∀ {n} → n ≮ 0
 n≮0 ()
 
@@ -412,7 +424,7 @@ n≮n : ∀ n → n ≮ n
 n≮n n = <-irrefl (refl {x = n})
 
 0<1+n : ∀ {n} → 0 < suc n
-0<1+n = s≤s z≤n
+0<1+n = z<s
 
 n<1+n : ∀ n → n < suc n
 n<1+n n = ≤-refl
@@ -436,6 +448,19 @@ m<n⇒n≢0 (s≤s m≤n) ()
 m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
 m<n⇒m≤1+n = ≤-step ∘ <⇒≤
 
+m<1+n⇒m<n∨m≡n :  ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
+m<1+n⇒m<n∨m≡n {0}     {0}     _          =  inj₂ refl
+m<1+n⇒m<n∨m≡n {0}     {suc n} _          =  inj₁ 0<1+n
+m<1+n⇒m<n∨m≡n {suc m} {suc n} (s<s m<1+n)  with m<1+n⇒m<n∨m≡n m<1+n
+... | inj₂ m≡n = inj₂ (cong suc m≡n)
+... | inj₁ m<n = inj₁ (s<s m<n)
+
+m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
+m≤n⇒m<n∨m≡n m≤n = m<1+n⇒m<n∨m≡n (s≤s m≤n)
+
+m<1+n⇒m≤n : ∀ {m n} → m < suc n → m ≤ n
+m<1+n⇒m≤n (s≤s m≤n) = m≤n
+
 ∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
 ∀[m≤n⇒m≢o]⇒n<o _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
 ∀[m≤n⇒m≢o]⇒n<o zero    (suc o) _       = 0<1+n
@@ -654,13 +679,6 @@ m≤m+n (suc m) n = s≤s (m≤m+n m n)
 m≤n+m : ∀ m n → m ≤ n + m
 m≤n+m m n = subst (m ≤_) (+-comm m n) (m≤m+n m n)
 
-m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
-m≤n⇒m<n∨m≡n {0}     {0}     _          =  inj₂ refl
-m≤n⇒m<n∨m≡n {0}     {suc n} _          =  inj₁ 0<1+n
-m≤n⇒m<n∨m≡n {suc m} {suc n} (s≤s m≤n)  with m≤n⇒m<n∨m≡n m≤n
-... | inj₂ m≡n = inj₂ (cong suc m≡n)
-... | inj₁ m<n = inj₁ (s≤s m<n)
-
 m+n≤o⇒m≤o : ∀ m {n o} → m + n ≤ o → m ≤ o
 m+n≤o⇒m≤o zero    m+n≤o       = z≤n
 m+n≤o⇒m≤o (suc m) (s≤s m+n≤o) = s≤s (m+n≤o⇒m≤o m m+n≤o)
@@ -680,8 +698,8 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 +-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o
 
 +-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
-+-mono-<-≤ {_} {suc n} (s≤s z≤n)       o≤p = s≤s (≤-stepsˡ n o≤p)
-+-mono-<-≤ {_} {_}     (s≤s (s≤s m<n)) o≤p = s≤s (+-mono-<-≤ (s≤s m<n) o≤p)
++-mono-<-≤ {_} {suc n} z<s               o≤p = s≤s (≤-stepsˡ n o≤p)
++-mono-<-≤ {_} {_}     (s<s m<n@(s≤s _)) o≤p = s≤s (+-mono-<-≤ m<n o≤p)
 
 +-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
 +-mono-≤-< {_} {n} z≤n       o<p = ≤-trans o<p (m≤n+m _ n)
@@ -698,18 +716,18 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 +-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)
 
 m+1+n≰m : ∀ m {n} → m + suc n ≰ m
-m+1+n≰m (suc m) le = m+1+n≰m m (≤-pred le)
+m+1+n≰m (suc m) (s≤s m+1+n≤m) = m+1+n≰m m m+1+n≤m
 
 m<m+n : ∀ m {n} → n > 0 → m < m + n
 m<m+n zero    n>0 = n>0
-m<m+n (suc m) n>0 = s≤s (m<m+n m n>0)
+m<m+n (suc m) n>0 = s<s (m<m+n m n>0)
 
 m<n+m : ∀ m {n} → n > 0 → m < n + m
 m<n+m m {n} n>0 rewrite +-comm n m = m<m+n m n>0
 
 m+n≮n : ∀ m n → m + n ≮ n
 m+n≮n zero    n                   = n≮n n
-m+n≮n (suc m) (suc n) (s≤s m+n<n) = m+n≮n m (suc n) (≤-step m+n<n)
+m+n≮n (suc m) (suc n) (s<s m+n<n) = m+n≮n m (suc n) (<-step m+n<n)
 
 m+n≮m : ∀ m n → m + n ≮ m
 m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
@@ -947,24 +965,23 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
 *-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
 
 *-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
-*-mono-< (s≤s z≤n)       (s≤s u≤v) = s≤s z≤n
-*-mono-< (s≤s (s≤s m≤n)) (s≤s u≤v) =
-  +-mono-< (s≤s u≤v) (*-mono-< (s≤s m≤n) (s≤s u≤v))
+*-mono-< z<s               u<v@(s≤s _) = 0<1+n
+*-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
 
 *-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
-*-monoˡ-< (suc n) (s≤s z≤n)       = s≤s z≤n
-*-monoˡ-< (suc n) (s≤s (s≤s m≤o)) =
-  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) (s≤s m≤o))
+*-monoˡ-< (suc n) z<s       = 0<1+n
+*-monoˡ-< (suc n) (s<s m<o@(s≤s _)) =
+  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< (suc n) m<o)
 
 *-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
-*-monoʳ-< (suc zero)    (s≤s m≤o) = +-mono-≤ (s≤s m≤o) z≤n
-*-monoʳ-< (suc (suc n)) (s≤s m≤o) =
-  +-mono-≤ (s≤s m≤o) (<⇒≤ (*-monoʳ-< (suc n) (s≤s m≤o)))
+*-monoʳ-< (suc zero)    m<o@(s≤s _) = +-mono-≤ m<o z≤n
+*-monoʳ-< (suc (suc n)) m<o@(s≤s _) =
+  +-mono-≤ m<o (<⇒≤ (*-monoʳ-< (suc n) m<o))
 
 m≤m*n : ∀ m n .{{_ : NonZero n}} → m ≤ m * n
 m≤m*n m n@(suc _) = begin
   m     ≡⟨ sym (*-identityʳ m) ⟩
-  m * 1 ≤⟨ *-monoʳ-≤ m (s≤s z≤n) ⟩
+  m * 1 ≤⟨ *-monoʳ-≤ m 0<1+n ⟩
   m * n ∎
 
 m≤n*m : ∀ m n .{{_ : NonZero n}} → m ≤ n * m
@@ -1863,15 +1880,15 @@ m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
 ⌊n/2⌋≤n (suc (suc n)) = s≤s (≤-step (⌊n/2⌋≤n n))
 
 ⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
-⌊n/2⌋<n zero    = s≤s z≤n
-⌊n/2⌋<n (suc n) = s≤s (s≤s (⌊n/2⌋≤n n))
+⌊n/2⌋<n zero    = z<s
+⌊n/2⌋<n (suc n) = s<s (s≤s (⌊n/2⌋≤n n))
 
 ⌈n/2⌉≤n : ∀ n → ⌈ n /2⌉ ≤ n
-⌈n/2⌉≤n zero = z≤n
+⌈n/2⌉≤n zero    = z≤n
 ⌈n/2⌉≤n (suc n) = s≤s (⌊n/2⌋≤n n)
 
 ⌈n/2⌉<n : ∀ n → ⌈ suc (suc n) /2⌉ < suc (suc n)
-⌈n/2⌉<n n = s≤s (⌊n/2⌋<n n)
+⌈n/2⌉<n n = s<s (⌊n/2⌋<n n)
 
 ------------------------------------------------------------------------
 -- Properties of !_
@@ -1888,7 +1905,6 @@ m !* n !≢0 = m*n≢0 _ _ {{m !≢0}} {{n !≢0}}
 
 ------------------------------------------------------------------------
 -- Properties of _≤′_ and _<′_
-------------------------------------------------------------------------
 
 ≤′-trans : Transitive _≤′_
 ≤′-trans m≤n ≤′-refl       = m≤n
@@ -1913,6 +1929,35 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
 ≤′-step-injective : ∀ {m n} {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q
 ≤′-step-injective refl = refl
 
+------------------------------------------------------------------------
+-- Properties of _<′_ and _<_
+------------------------------------------------------------------------
+
+z<′s : ∀ {n} → zero <′ suc n
+z<′s {zero}  = <′-base
+z<′s {suc n} = <′-step (z<′s {n})
+
+s<′s : ∀ {m n} → m <′ n → suc m <′ suc n
+s<′s <′-base        = <′-base
+s<′s (<′-step m<′n) = <′-step (s<′s m<′n)
+
+<⇒<′ : ∀ {m n} → m < n → m <′ n
+<⇒<′ z<s               = z<′s
+<⇒<′ (s<s m<n@(s≤s _)) = s<′s (<⇒<′ m<n)
+
+<′⇒< : ∀ {m n} → m <′ n → m < n
+<′⇒< <′-base        = n<1+n _
+<′⇒< (<′-step m<′n) = <-step (<′⇒< m<′n)
+
+m<1+n⇒m<n∨m≡n′ : ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
+m<1+n⇒m<n∨m≡n′ m<n with <⇒<′ m<n
+... | <′-base      = inj₂ refl
+... | <′-step m<′n = inj₁ (<′⇒< m<′n)
+
+------------------------------------------------------------------------
+-- Other properties of _≤′_ and _<′_
+------------------------------------------------------------------------
+
 infix 4 _≤′?_ _<′?_ _≥′?_ _>′?_
 
 _≤′?_ : Decidable _≤′_
@@ -2075,9 +2120,9 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   ... | no ¬Pv | no ¬Pn<v           = no ¬Pn<1+v
     where
     ¬Pn<1+v : ∄ λ n → n < suc v × P n
-    ¬Pn<1+v (n , n<1+v , Pn) with n ≟ v
+    ¬Pn<1+v (n , s≤s n≤v , Pn) with n ≟ v
     ... | yes refl = ¬Pv Pn
-    ... | no  n≢v  = ¬Pn<v (n , ≤∧≢⇒< (≤-pred n<1+v) n≢v , Pn)
+    ... | no  n≢v  = ¬Pn<v (n , ≤∧≢⇒< n≤v n≢v , Pn)
 
   allUpTo? : ∀ v → Dec (∀ {n} → n < v → P n)
   allUpTo? zero    = yes λ()
@@ -2087,9 +2132,9 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   ... | yes Pn | yes Pn<v = yes Pn<1+v
     where
       Pn<1+v : ∀ {n} → n < suc v → P n
-      Pn<1+v {n} n<1+v with n ≟ v
+      Pn<1+v {n} (s≤s n≤v) with n ≟ v
       ... | yes refl = Pn
-      ... | no  n≢v  = Pn<v (≤∧≢⇒< (≤-pred n<1+v) n≢v)
+      ... | no  n≢v  = Pn<v (≤∧≢⇒< n≤v n≢v)
 
 
 
@@ -2197,3 +2242,4 @@ suc[pred[n]]≡n {suc n} _   = refl
 {-# WARNING_ON_USAGE suc[pred[n]]≡n
 "Warning: suc[pred[n]]≡n was deprecated in v2.0. Please use suc-pred instead. Note that the proof now uses instance arguments"
 #-}
+
diff --git a/src/Data/Nat/Properties/Core.agda b/src/Data/Nat/Properties/Core.agda
index f7386d4d9d..66341f0160 100644
--- a/src/Data/Nat/Properties/Core.agda
+++ b/src/Data/Nat/Properties/Core.agda
@@ -1,13 +1,20 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- ≤-pred definition so as to not cause dependency problems.
+-- This module is DEPRECATED. Please use
+-- `Data.Nat.Properties` directly.
+--
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Nat.Properties.Core where
 
+{-# WARNING_ON_IMPORT
+"Data.Nat.Properties.Core was deprecated in v2.0.
+Use Data.Nat.Properties instead."
+#-}
+
 open import Data.Nat.Base
 
 ------------------------------------------------------------------------
@@ -16,3 +23,4 @@ open import Data.Nat.Base
 
 ≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
 ≤-pred (s≤s m≤n) = m≤n
+
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index c7cdf154e4..2b32f0942d 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -219,7 +219,7 @@ lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m
                       lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
 lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs)
   rewrite unfold-take m x xs = refl
-lookup-inject≤-take (suc (suc m)) m≤m+n (suc zero) (x ∷ y ∷ xs)
+lookup-inject≤-take (suc (suc m)) (s≤s m≤m+n) (suc zero) (x ∷ y ∷ xs)
   rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = refl
 lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ y ∷ xs)
   rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = lookup-inject≤-take m m≤m+n i xs
@@ -456,9 +456,8 @@ map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs)
 lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i<m : toℕ i < m) →
               lookup (xs ++ ys) i  ≡ lookup xs (Fin.fromℕ< i<m)
-lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
-lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
-  lookup-++-< xs ys i (s≤s i<m)
+lookup-++-< (x ∷ xs) ys zero    z<s       = refl
+lookup-++-< (x ∷ xs) ys (suc i) (s<s i<m) = lookup-++-< xs ys i i<m
 
 lookup-++-≥ : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i≥m : toℕ i ≥ m) →