diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3d99a6eb2b..b1aa32b023 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1260,7 +1260,7 @@ Deprecated modules
 
 ### Deprecation of `Data.Nat.Properties.Core`
 
-* The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties`
+* The module `Data.Nat.Properties.Core` has been deprecated, and its one lemma moved to `Data.Nat.Base`, renamed as `s≤s⁻¹`
 
 ### Deprecation of `Data.Fin.Substitution.Example`
 
@@ -1527,6 +1527,7 @@ Deprecated names
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o
   <-step          ↦  m<n⇒m<1+n
+  pred-mono       ↦  pred-mono-≤
 
   <-transʳ        ↦  ≤-<-trans
   <-transˡ        ↦  <-≤-trans
@@ -2593,9 +2594,18 @@ Additions to existing modules
   pattern z<s {n}         = s≤s (z≤n {n})
   pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
+  s≤s⁻¹ : suc m ≤ suc n → m ≤ n
+  s<s⁻¹ : suc m < suc n → m < n
+
   pattern <′-base          = ≤′-refl
   pattern <′-step {n} m<′n = ≤′-step {n} m<′n
 
+  pattern ≤″-offset k = less-than-or-equal {k} refl
+  pattern <″-offset k = ≤″-offset k
+
+  s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
+  s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
+
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
@@ -2646,12 +2656,13 @@ Additions to existing modules
   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
 
+  pred-mono-≤   : m ≤ n → pred m ≤ pred n
+  pred-mono-<   : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
   <⇒<′ : m < n → m <′ n
diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda
index 113bdde6ca..fb52d2af72 100644
--- a/src/Data/Digit/Properties.agda
+++ b/src/Data/Digit/Properties.agda
@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
+open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 2d5b0f638e..9b4c303f2f 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -11,17 +11,16 @@
 
 module Data.Fin.Base where
 
-open import Data.Bool.Base using (Bool; true; false; T; not)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Bool.Base using (Bool; T)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation.Core using (contradiction)
-open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable
@@ -68,16 +67,15 @@ fromℕ (suc n) = suc (fromℕ n)
 
 -- fromℕ< {m} _ = "m".
 
-fromℕ< : m ℕ.< n → Fin n
-fromℕ< {zero}  {suc n} z<s = zero
-fromℕ< {suc m} {suc n} (s<s m<n) = suc (fromℕ< m<n)
+fromℕ< : .(m ℕ.< n) → Fin n
+fromℕ< {zero}  {suc _} _   = zero
+fromℕ< {suc m} {suc _} m<n = suc (fromℕ< (ℕ.s<s⁻¹ m<n))
 
 -- fromℕ<″ m _ = "m".
 
-fromℕ<″ : ∀ m {n} → m ℕ.<″ n → Fin n
-fromℕ<″ zero    (ℕ.less-than-or-equal refl) = zero
-fromℕ<″ (suc m) (ℕ.less-than-or-equal refl) =
-  suc (fromℕ<″ m (ℕ.less-than-or-equal refl))
+fromℕ<″ : ∀ m {n} → .(m ℕ.<″ n) → Fin n
+fromℕ<″ zero    {suc _} _    = zero
+fromℕ<″ (suc m) {suc _} m<″n = suc (fromℕ<″ m (ℕ.s<″s⁻¹ m<″n))
 
 -- canonical liftings of i:Fin m to larger index
 
@@ -95,9 +93,9 @@ zero    ↑ʳ i = i
 
 -- reduce≥ "m + i" _ = "i".
 
-reduce≥ : ∀ (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) → Fin n
-reduce≥ {zero}  i       i≥m       = i
-reduce≥ {suc m} (suc i) (s≤s i≥m) = reduce≥ i i≥m
+reduce≥ : ∀ (i : Fin (m ℕ.+ n)) → .(m ℕ.≤ toℕ i) → Fin n
+reduce≥ {zero}  i       _   = i
+reduce≥ {suc _} (suc i) m≤i = reduce≥ i (ℕ.s≤s⁻¹ m≤i)
 
 -- inject⋆ m "i" = "i".
 
@@ -106,16 +104,16 @@ inject {i = suc i} zero    = zero
 inject {i = suc i} (suc j) = suc (inject j)
 
 inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
-inject! {n = suc _} {i = suc _}  zero    = zero
-inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)
+inject! {n = suc _} {i = suc _} zero    = zero
+inject! {n = suc _} {i = suc _} (suc j) = suc (inject! j)
 
 inject₁ : Fin n → Fin (suc n)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
-inject≤ : Fin m → m ℕ.≤ n → Fin n
-inject≤ {_} {suc n} zero    _         =  zero
-inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
+inject≤ : Fin m → .(m ℕ.≤ n) → Fin n
+inject≤ {n = suc _} zero    _   = zero
+inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n))
 
 -- lower₁ "i" _ = "i".
 
@@ -166,12 +164,12 @@ combine {suc m} {n} zero    j = j ↑ˡ (m ℕ.* n)
 combine {suc m} {n} (suc i) j = n ↑ʳ (combine i j)
 
 -- Next in progression after splitAt and remQuot
-finToFun : Fin (m ^ n) → (Fin n → Fin m)
-finToFun {m} {suc n} i zero    = quotient (m ^ n) i
-finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ^ n) i) j
+finToFun : Fin (m ℕ.^ n) → (Fin n → Fin m)
+finToFun {m} {suc n} i zero    = quotient (m ℕ.^ n) i
+finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ℕ.^ n) i) j
 
 -- inverse of above function
-funToFin : (Fin m → Fin n) → Fin (n ^ m)
+funToFin : (Fin m → Fin n) → Fin (n ℕ.^ m)
 funToFin {zero}  f = zero
 funToFin {suc m} f = combine (f zero) (funToFin (f ∘ suc))
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ef2073269f..ea7c43c90f 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -19,7 +19,7 @@ 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; z<s; s<s; _∸_; _^_)
+  using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
@@ -43,10 +43,10 @@ open import Relation.Binary.Structures
   using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning)
-open import Relation.Nullary
-  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_; _×-dec_; _⊎-dec_; contradiction)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable as Dec using (map′)
+open import Relation.Nullary.Decidable as Dec
+  using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (Reflects; invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -162,6 +162,10 @@ toℕ-↑ʳ (suc n) i = cong suc (toℕ-↑ʳ n i)
 -- toℕ and the ordering relations
 ------------------------------------------------------------------------
 
+toℕ<n : ∀ (i : Fin n) → toℕ i ℕ.< n
+toℕ<n {n = suc _} zero    = z<s
+toℕ<n {n = suc _} (suc i) = s<s (toℕ<n i)
+
 toℕ≤pred[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)
@@ -169,9 +173,6 @@ toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)
 toℕ≤n : ∀ (i : Fin n) → toℕ i ℕ.≤ n
 toℕ≤n {suc n} i = ℕₚ.m≤n⇒m≤1+n (toℕ≤pred[n] i)
 
-toℕ<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],
@@ -203,37 +204,38 @@ fromℕ-toℕ : ∀ (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
 fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
-≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
-≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i)
+≤fromℕ : ∀ (i : Fin (suc n)) → i ≤ fromℕ n
+≤fromℕ {n = n} i rewrite toℕ-fromℕ n = ℕ.s≤s⁻¹ (toℕ<n i)
 
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
 
-fromℕ<-toℕ : ∀ (i : Fin n) (i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
-fromℕ<-toℕ zero    z<s       = refl
-fromℕ<-toℕ (suc i) (s<s i<n) = cong suc (fromℕ<-toℕ i i<n)
+fromℕ<-toℕ : ∀ (i : Fin n) .(i<n : toℕ i ℕ.< n) → fromℕ< i<n ≡ i
+fromℕ<-toℕ zero    _   = refl
+fromℕ<-toℕ (suc i) i<n = cong suc (fromℕ<-toℕ i (ℕ.s<s⁻¹ i<n))
 
-toℕ-fromℕ< : ∀ (m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
-toℕ-fromℕ< z<s               = refl
-toℕ-fromℕ< (s<s m<n@(s≤s _)) = cong suc (toℕ-fromℕ< m<n)
+toℕ-fromℕ< : ∀ .(m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
+toℕ-fromℕ< {m = zero}  {n = suc _} _   = refl
+toℕ-fromℕ< {m = suc m} {n = suc _} m<n = cong suc (toℕ-fromℕ< (ℕ.s<s⁻¹ m<n))
 
 -- fromℕ is a special case of fromℕ<.
 fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
 fromℕ-def zero    = refl
 fromℕ-def (suc n) = cong suc (fromℕ-def n)
 
-fromℕ<-cong : ∀ m n {o} → m ≡ n → (m<o : m ℕ.< o) (n<o : n ℕ.< o) →
+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 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ℕ<-cong 0       0                   _ _   _   = refl
+fromℕ<-cong (suc _) (suc _) {o = suc _} r m<n n<o
+  = cong suc (fromℕ<-cong _ _ (ℕₚ.suc-injective r) (ℕ.s<s⁻¹ m<n) (ℕ.s<s⁻¹ n<o))
 
-fromℕ<-injective : ∀ m n {o} → (m<o : m ℕ.< o) (n<o : 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       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ℕ<-injective 0       0                   _   _   _  = refl
+fromℕ<-injective 0       (suc _) {o = suc _} _ _ ()
+fromℕ<-injective (suc _) (suc _) {o = suc _} m<n n<o r
+  = cong suc (fromℕ<-injective _ _ (ℕ.s<s⁻¹ m<n) (ℕ.s<s⁻¹ n<o) (suc-injective r))
 
 ------------------------------------------------------------------------
 -- fromℕ<″
@@ -241,9 +243,9 @@ fromℕ<-injective (suc _) (suc _) (s<s m<n@(s≤s _)) (s<s n<o@(s≤s _)) r
 
 fromℕ<≡fromℕ<″ : ∀ (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                  fromℕ< m<n ≡ fromℕ<″ m m<″n
-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))
+fromℕ<≡fromℕ<″ {m = zero}  m<n (ℕ.<″-offset _) = refl
+fromℕ<≡fromℕ<″ {m = suc m} m<n (ℕ.<″-offset _)
+  = cong suc (fromℕ<≡fromℕ<″ (ℕ.s<s⁻¹ m<n) (ℕ.<″-offset _))
 
 toℕ-fromℕ<″ : ∀ (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
 toℕ-fromℕ<″ {m} {n} m<n = begin
@@ -375,9 +377,9 @@ m <? n = suc (toℕ m) ℕₚ.≤? toℕ n
 <-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≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)
+... | tri< i<j i≢j j≮i = tri< (s<s i<j)     (i≢j ∘ suc-injective) (j≮i ∘ s<s⁻¹)
+... | tri> i≮j i≢j j<i = tri> (i≮j ∘ s<s⁻¹) (i≢j ∘ suc-injective) (s<s j<i)
+... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ s<s⁻¹) (cong suc i≡j)        (j≮i ∘ s<s⁻¹)
 
 <-respˡ-≡ : (_<_ {m} {n}) Respectsˡ _≡_
 <-respˡ-≡ refl x≤y = x≤y
@@ -432,10 +434,10 @@ i<1+i = ℕₚ.n<1+n ∘ toℕ
 <⇒≢ i<i refl = ℕₚ.n≮n _ i<i
 
 ≤∧≢⇒< : i ≤ j → i ≢ j → i < j
-≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
-≤∧≢⇒< {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)))
+≤∧≢⇒< {i = zero}  {zero}  _         0≢0   = contradiction refl 0≢0
+≤∧≢⇒< {i = zero}  {suc j} _         _     = z<s
+≤∧≢⇒< {i = suc i} {suc j} 1+i≤1+j 1+i≢1+j =
+  s<s (≤∧≢⇒< (ℕ.s≤s⁻¹ 1+i≤1+j) (1+i≢1+j ∘ (cong suc)))
 
 ------------------------------------------------------------------------
 -- inject
@@ -474,11 +476,11 @@ inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 ≤̄⇒inject₁< {i = i} i≤j rewrite sym (toℕ-inject₁ i) = s<s i≤j
 
 ℕ<⇒inject₁< : ∀ {i : Fin (ℕ.suc n)} {j : Fin n} → j < i → inject₁ j < i
-ℕ<⇒inject₁< {i = suc i} (s≤s j≤i) = ≤̄⇒inject₁< j≤i
+ℕ<⇒inject₁< {i = suc i} j≤i = ≤̄⇒inject₁< (ℕ.s≤s⁻¹ j≤i)
 
 i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j
-i≤inject₁[j]⇒i≤1+j {i = zero} i≤j = z≤n
-i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} (s≤s i≤j) = s≤s (ℕₚ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) i≤j))
+i≤inject₁[j]⇒i≤1+j {i = zero}              _   = z≤n
+i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} i≤j = s≤s (ℕₚ.m≤n⇒m≤1+n (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) (ℕ.s≤s⁻¹ i≤j)))
 
 ------------------------------------------------------------------------
 -- lower₁
@@ -491,8 +493,8 @@ toℕ-lower₁ {ℕ.suc m} (suc i) p = cong ℕ.suc (toℕ-lower₁ i (p ∘ con
 
 lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
                    lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
-lower₁-injective {zero}  {zero}  {_}     {n≢i} {_}   _    = ⊥-elim (n≢i refl)
-lower₁-injective {zero}  {_}     {zero}  {_}   {n≢j} _    = ⊥-elim (n≢j refl)
+lower₁-injective {zero}  {zero}  {_}     {n≢i} {_}   _    = contradiction refl n≢i
+lower₁-injective {zero}  {_}     {zero}  {_}   {n≢j} _    = contradiction refl n≢j
 lower₁-injective {suc n} {zero}  {zero}  {_}   {_}   refl = refl
 lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq   =
   cong suc (lower₁-injective (suc-injective eq))
@@ -532,34 +534,34 @@ inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-l
 -- inject≤
 ------------------------------------------------------------------------
 
-toℕ-inject≤ : ∀ i (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)
+toℕ-inject≤ : ∀ i .(m≤n : m ℕ.≤ n) → toℕ (inject≤ i m≤n) ≡ toℕ i
+toℕ-inject≤ {_} {suc n} zero    _ = refl
+toℕ-inject≤ {_} {suc n} (suc i) _ = cong suc (toℕ-inject≤ i _)
 
-inject≤-refl : ∀ i (n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
-inject≤-refl {suc n} zero    _         = refl
-inject≤-refl {suc n} (suc i) (s≤s n≤n) = cong suc (inject≤-refl i n≤n)
+inject≤-refl : ∀ i .(n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
+inject≤-refl {suc n} zero    _   = refl
+inject≤-refl {suc n} (suc i) _ = cong suc (inject≤-refl i _)
 
 inject≤-idempotent : ∀ (i : Fin m)
-                     (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) (m≤o : m ℕ.≤ o) →
+                     .(m≤n : m ℕ.≤ n) .(n≤o : n ℕ.≤ o) .(m≤o : m ℕ.≤ o) →
                      inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i m≤o
-inject≤-idempotent {_} {suc n} {suc o} zero    _   _   _ = refl
-inject≤-idempotent {_} {suc n} {suc o} (suc i) (s≤s m≤n) (s≤s n≤o) (s≤s m≤o) =
-  cong suc (inject≤-idempotent i m≤n n≤o m≤o)
+inject≤-idempotent {_} {suc n} {suc o} zero    _ _ _ = refl
+inject≤-idempotent {_} {suc n} {suc o} (suc i) _ _ _ =
+  cong suc (inject≤-idempotent i _ _ _)
 
-inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) →
+inject≤-trans : ∀ (i : Fin m) .(m≤n : m ℕ.≤ n) .(n≤o : n ℕ.≤ o) →
                 inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o)
-inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _
+inject≤-trans i _ _ = inject≤-idempotent i _ _ _
 
-inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j →
+inject≤-injective : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i j →
                     inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j
-inject≤-injective (s≤s p) (s≤s q) zero    zero    eq = refl
-inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq =
-  cong suc (inject≤-injective p q i j (suc-injective eq))
+inject≤-injective {n = suc _} _ _ zero    zero    eq = refl
+inject≤-injective {n = suc _} _ _ (suc i) (suc j) eq =
+  cong suc (inject≤-injective _ _ i j (suc-injective eq))
 
-inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i →
+inject≤-irrelevant : ∀ .(m≤n m≤n′ : m ℕ.≤ n) i →
                     inject≤ i m≤n ≡ inject≤ i m≤n′
-inject≤-irrelevant m≤n m≤n′ i =  cong (inject≤ i) (ℕₚ.≤-irrelevant m≤n m≤n′)
+inject≤-irrelevant _ _ i = refl
 
 ------------------------------------------------------------------------
 -- pred
@@ -581,8 +583,10 @@ splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl
 
 splitAt⁻¹-↑ˡ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i
 splitAt⁻¹-↑ˡ {suc m} {n} {0F} {.0F} refl = refl
-splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₁[j]
-... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j])
+splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq
+  with inj₁ k ← splitAt m i in splitAt[m][i]≡inj₁[j]
+  with refl ← eq
+  = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j])
 
 splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i
 splitAt-↑ʳ zero    n i = refl
@@ -590,8 +594,10 @@ splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl
 
 splitAt⁻¹-↑ʳ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i
 splitAt⁻¹-↑ʳ {zero}  {n} {i} {j} refl = refl
-splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₂[k]
-... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k])
+splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq
+  with inj₂ k ← splitAt m i in splitAt[m][i]≡inj₂[k]
+  with refl ← eq
+  = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k])
 
 splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i
 splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n
@@ -609,17 +615,17 @@ join-splitAt (suc m) n (suc i) = begin
 
 -- splitAt "m" "i" ≡ inj₁ "i" if i < m
 
-splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) (i<m : toℕ i ℕ.< m) →
+splitAt-< : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i<m : toℕ i ℕ.< m) →
             splitAt m i ≡ inj₁ (fromℕ< 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-< (suc m) zero    _   = refl
+splitAt-< (suc m) (suc i) i<m = cong (Sum.map suc id) (splitAt-< m i (ℕ.s<s⁻¹ i<m))
 
 -- splitAt "m" "i" ≡ inj₂ "i - m" if i ≥ m
 
-splitAt-≥ : ∀ m {n} (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m) →
+splitAt-≥ : ∀ m {n} (i : Fin (m ℕ.+ n)) .(i≥m : toℕ i ℕ.≥ m) →
             splitAt m i ≡ inj₂ (reduce≥ i i≥m)
-splitAt-≥ zero    i       _         = refl
-splitAt-≥ (suc m) (suc i) (s≤s i≥m) = cong (Sum.map suc id) (splitAt-≥ m i i≥m)
+splitAt-≥ zero    i       _   = refl
+splitAt-≥ (suc m) (suc i) i≥m = cong (Sum.map suc id) (splitAt-≥ m i (ℕ.s≤s⁻¹ i≥m))
 
 ------------------------------------------------------------------------
 -- Bundles
@@ -691,8 +697,9 @@ combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ with <-cmp i k
 
 combine-injectiveʳ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → j ≡ l
-combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ with combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
-... | refl = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
+combine-injectiveʳ {m} {n} i j k l cᵢⱼ≡cₖₗ
+  with refl ← combine-injectiveˡ i j k l cᵢⱼ≡cₖₗ
+  = toℕ-injective (ℕₚ.+-cancelˡ-≡ (n ℕ.* toℕ i) _ _ (begin
   n ℕ.* toℕ i ℕ.+ toℕ j ≡˘⟨ toℕ-combine i j ⟩
   toℕ (combine i j)     ≡⟨ cong toℕ cᵢⱼ≡cₖₗ ⟩
   toℕ (combine i l)     ≡⟨ toℕ-combine i l ⟩
@@ -706,8 +713,8 @@ combine-injective i j k l cᵢⱼ≡cₖₗ =
   combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ
 
 combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i
-combine-surjective {m} {n} i with remQuot {m} n i in eq
-... | j , k = j , k , (begin
+combine-surjective {m} {n} i with j , k ← remQuot {m} n i in eq
+  = j , k , (begin
   combine j k                       ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩
   uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩
   i                                 ∎)
@@ -891,10 +898,10 @@ pinch-surjective zero    (suc j) = suc (suc j) , λ { refl → refl }
 pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j)
 
 pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
-pinch-mono-≤ 0F      {0F}    {k}     0≤n       = z≤n
-pinch-mono-≤ 0F      {suc j} {suc k} (s≤s j≤k) = j≤k
-pinch-mono-≤ (suc i) {0F}    {k}     0≤n       = z≤n
-pinch-mono-≤ (suc i) {suc j} {suc k} (s≤s j≤k) = s≤s (pinch-mono-≤ i j≤k)
+pinch-mono-≤ 0F      {0F}    {k}     0≤n = z≤n
+pinch-mono-≤ 0F      {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k
+pinch-mono-≤ (suc i) {0F}    {k}     0≤n = z≤n
+pinch-mono-≤ (suc i) {suc j} {suc k} j≤k = s≤s (pinch-mono-≤ i (ℕ.s≤s⁻¹ j≤k))
 
 pinch-injective : ∀ {i : Fin n} {j k : Fin (ℕ.suc n)} →
                   suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
@@ -963,8 +970,8 @@ private
   -- The boolean component of the result is exactly the
   -- obvious fold of boolean tests (`foldr _∧_ true`).
   note : ∀ {p} {P : Pred (Fin 3) p} (P? : Decidable P) →
-         ∃ λ z → does (all? P?) ≡ z
-  note P? = does (P? 0F) ∧ does (P? 1F) ∧ does (P? 2F) ∧ true
+         ∃ λ z → Dec.does (all? P?) ≡ z
+  note P? = Dec.does (P? 0F) ∧ Dec.does (P? 1F) ∧ Dec.does (P? 2F) ∧ true
           , refl
 
 -- If a decidable predicate P over a finite set is sometimes false,
@@ -995,10 +1002,9 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 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 , z<s , f₀≡fⱼ
-... | no  f₀≢fₖ with pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
-...   | (i , j , i<j , fᵢ≡fⱼ) =
-  suc i , suc j , s<s i<j ,
-  punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
+... | no  f₀≢fₖ
+  with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
+  = suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
 
 injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
 injective⇒≤ {zero}  {_}     {f} _   = z≤n
@@ -1087,7 +1093,7 @@ opposite-suc {n} i = begin
   toℕ (opposite (suc i))     ≡⟨ opposite-prop (suc i) ⟩
   suc n ∸ suc (toℕ (suc i))  ≡⟨⟩
   n ∸ toℕ (suc i)            ≡⟨⟩
-  n ∸ suc (toℕ i)            ≡⟨ sym (opposite-prop i) ⟩
+  n ∸ suc (toℕ i)            ≡˘⟨ opposite-prop i ⟩
   toℕ (opposite i)           ∎
   where open ≡-Reasoning
 
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 8dfa60de79..21b3f3d71c 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -16,8 +16,8 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
-open import Data.Nat as ℕ
-  using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s)
+open import Data.Nat.Base as ℕ
+  using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s; s≤s⁻¹; s<s⁻¹)
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
@@ -302,9 +302,9 @@ drop‿-<- (-<- n<m) = n<m
 ... | tri≈ m≮n m≡n n≯m = tri≈ (n≯m ∘ drop‿-<-) (cong -[1+_] m≡n) (m≮n ∘ drop‿-<-)
 ... | tri> m≮n m≢n n>m = tri< (-<- n>m) (m≢n ∘ -[1+-injective) (m≮n ∘ drop‿-<-)
 <-cmp +[1+ m ] +[1+ n ] with ℕ.<-cmp m n
-... | tri< m<n m≢n n≯m = tri< (+<+ (s<s m<n))              (m≢n ∘ +[1+-injective) (n≯m ∘ ℕ.≤-pred ∘ drop‿+<+)
-... | tri≈ m≮n m≡n n≯m = tri≈ (m≮n ∘ ℕ.≤-pred ∘ drop‿+<+) (cong (+_ ∘ suc) m≡n)  (n≯m ∘ ℕ.≤-pred ∘ drop‿+<+)
-... | tri> m≮n m≢n n>m = tri> (m≮n ∘ ℕ.≤-pred ∘ drop‿+<+) (m≢n ∘ +[1+-injective) (+<+ (s<s n>m))
+... | tri< m<n m≢n n≯m = tri< (+<+ (s<s m<n))              (m≢n ∘ +[1+-injective) (n≯m ∘ s<s⁻¹ ∘ drop‿+<+)
+... | tri≈ m≮n m≡n n≯m = tri≈ (m≮n ∘ s<s⁻¹ ∘ drop‿+<+) (cong (+_ ∘ suc) m≡n)  (n≯m ∘ s<s⁻¹ ∘ drop‿+<+)
+... | tri> m≮n m≢n n>m = tri> (m≮n ∘ s<s⁻¹ ∘ drop‿+<+) (m≢n ∘ +[1+-injective) (+<+ (s<s n>m))
 
 infix 4 _<?_
 _<?_ : Decidable _<_
@@ -433,7 +433,7 @@ neg-mono-< { -[1+ _ ]} { -[1+ _ ]} (-<- n<m) = +<+ (s<s n<m)
 neg-mono-< { -[1+ _ ]} { +0}       -<+       = +<+ z<s
 neg-mono-< { -[1+ _ ]} { +[1+ n ]} -<+       = -<+
 neg-mono-< { +0}       { +[1+ n ]} (+<+ _)   = -<+
-neg-mono-< { +[1+ m ]} { +[1+ n ]} (+<+ m<n) = -<- (ℕ.≤-pred m<n)
+neg-mono-< { +[1+ m ]} { +[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 
 neg-cancel-< : - i < - j → i > j
 neg-cancel-< { +[1+ m ]} { +[1+ n ]} (-<- n<m)       = +<+ (s<s n<m)
@@ -442,7 +442,7 @@ neg-cancel-< { +[1+ m ]} { -[1+ n ]}  -<+            = -<+
 neg-cancel-< { +0}       { +0}       (+<+ ())
 neg-cancel-< { +0}       { -[1+ n ]} _               = -<+
 neg-cancel-< { -[1+ m ]} { +0}       (+<+ ())
-neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ (s<s m<n)) = -<- m<n
+neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
 
 ------------------------------------------------------------------------
 -- Properties of ∣_∣
@@ -1233,12 +1233,12 @@ suc[i]≤j⇒i<j : sucℤ i ≤ j → i < j
 suc[i]≤j⇒i<j {+ i}           {+ _}       (+≤+ i≤j) = +<+ i≤j
 suc[i]≤j⇒i<j { -[1+ 0 ]}     {+ j}       p         = -<+
 suc[i]≤j⇒i<j { -[1+ suc i ]} {+ j}       -≤+       = -<+
-suc[i]≤j⇒i<j { -[1+ suc i ]} { -[1+ j ]} (-≤- j≤i) = -<- (ℕ.s≤s j≤i)
+suc[i]≤j⇒i<j { -[1+ suc i ]} { -[1+ j ]} (-≤- j≤i) = -<- (s≤s j≤i)
 
 i<j⇒suc[i]≤j : i < j → sucℤ i ≤ j
 i<j⇒suc[i]≤j {+ _}           {+ _}       (+<+ i<j) = +≤+ i<j
 i<j⇒suc[i]≤j { -[1+ 0 ]}     {+ _}       -<+       = +≤+ z≤n
-i<j⇒suc[i]≤j { -[1+ suc i ]} { -[1+ _ ]} (-<- j<i) = -≤- (ℕ.≤-pred j<i)
+i<j⇒suc[i]≤j { -[1+ suc i ]} { -[1+ _ ]} (-<- j<i) = -≤- (s≤s⁻¹ j<i)
 i<j⇒suc[i]≤j { -[1+ suc i ]} {+ _}       -<+       = -≤+
 
 ------------------------------------------------------------------------
@@ -1288,7 +1288,7 @@ i≤pred[j]⇒i<j {_} { -[1+ n ]} leq = ≤-<-trans leq (-<- ℕ.≤-refl)
 i<j⇒i≤pred[j] : i < j → i ≤ pred j
 i<j⇒i≤pred[j] {_} { +0}       -<+       = -≤- z≤n
 i<j⇒i≤pred[j] {_} { +[1+ n ]} -<+       = -≤+
-i<j⇒i≤pred[j] {_} { +[1+ n ]} (+<+ m<n) = +≤+ (ℕ.≤-pred m<n)
+i<j⇒i≤pred[j] {_} { +[1+ n ]} (+<+ m<n) = +≤+ (s≤s⁻¹ m<n)
 i<j⇒i≤pred[j] {_} { -[1+ n ]} (-<- n<m) = -≤- n<m
 
 i≤j⇒pred[i]≤j : i ≤ j → pred i ≤ j
@@ -1723,7 +1723,7 @@ neg-distribʳ-* i j = begin
 
 *-cancelʳ-≤-pos : ∀ i j k .{{_ : Positive k}} → i * k ≤ j * k → i ≤ j
 *-cancelʳ-≤-pos -[1+ m ] -[1+ n ] +[1+ o ] (-≤- n≤m) =
-  -≤- (ℕ.≤-pred (ℕ.*-cancelʳ-≤ (suc n) (suc m) (suc o) (s≤s n≤m)))
+  -≤- (s≤s⁻¹ (ℕ.*-cancelʳ-≤ (suc n) (suc m) (suc o) (s≤s n≤m)))
 *-cancelʳ-≤-pos -[1+ _ ] (+ _)    +[1+ o ] _         = -≤+
 *-cancelʳ-≤-pos +0       +0       +[1+ o ] _         = +≤+ z≤n
 *-cancelʳ-≤-pos +0       +[1+ _ ] +[1+ o ] _         = +≤+ z≤n
@@ -1738,7 +1738,7 @@ neg-distribʳ-* i j = begin
 *-monoʳ-≤-nonNeg +0 {i} {j} i≤j rewrite *-zeroʳ i | *-zeroʳ j = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = 0})         = -≤+
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = suc _})     = -≤+
-*-monoʳ-≤-nonNeg +[1+ n ] (-≤- n≤m) = -≤- (ℕ.≤-pred (ℕ.*-mono-≤ (s≤s n≤m) (ℕ.≤-refl {x = suc n})))
+*-monoʳ-≤-nonNeg +[1+ n ] (-≤- n≤m) = -≤- (s≤s⁻¹ (ℕ.*-mono-≤ (s≤s n≤m) (ℕ.≤-refl {x = suc n})))
 *-monoʳ-≤-nonNeg +[1+ n ] {+0}       {+0}       (+≤+ m≤n) = +≤+ m≤n
 *-monoʳ-≤-nonNeg +[1+ n ] {+0}       {+[1+ _ ]} (+≤+ m≤n) = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] {+[1+ _ ]} {+[1+ _ ]} (+≤+ m≤n) = +≤+ (ℕ.*-monoˡ-≤ (suc n) m≤n)
@@ -1788,7 +1788,7 @@ neg-distribʳ-* i j = begin
 *-cancelˡ-<-nonNeg {+ i}       {+ j}       (+ n) leq = +<+ (ℕ.*-cancelˡ-< n _ _ (+◃-cancel-< leq))
 *-cancelˡ-<-nonNeg {+ i}       { -[1+ j ]} (+ n) leq = contradiction leq +◃≮-◃
 *-cancelˡ-<-nonNeg { -[1+ i ]} {+ j}       (+ n)leq = -<+
-*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (ℕ.≤-pred (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
+*-cancelˡ-<-nonNeg { -[1+ i ]} { -[1+ j ]} (+ n) leq = -<- (s<s⁻¹ (ℕ.*-cancelˡ-< n _ _ (neg◃-cancel-< leq)))
 
 *-cancelʳ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → i * k < j * k → i < j
 *-cancelʳ-<-nonNeg {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-<-nonNeg k
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5afce0cd54..78fc03f865 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -850,7 +850,7 @@ drop-drop (suc m) n (x ∷ xs) = drop-drop m n xs
 
 drop-all : (n : ℕ) (xs : List A) → n ≥ length xs → drop n xs ≡ []
 drop-all n       []       _ = drop-[] n
-drop-all (suc n) (x ∷ xs) p = drop-all n xs (≤-pred p)
+drop-all (suc n) (x ∷ xs) p = drop-all n xs (s≤s⁻¹ p)
 
 ------------------------------------------------------------------------
 -- replicate
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 10ece2fdb3..563448730c 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -17,7 +17,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
 open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
-open import Data.Nat.Properties using (≤-refl; ≤-pred; m≤n⇒m≤1+n)
+open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; nothing; just-nothing; nothing-just)
 open import Level using (Level)
diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 1abd7d9d7c..8811565c11 100644
--- a/src/Data/Nat.agda
+++ b/src/Data/Nat.agda
@@ -42,5 +42,8 @@ open import Data.Nat.Properties public
 
 -- Version 0.17
 
+-- Version 2.0
+
+-- solely for the re-export of this name, formerly in `Data.Nat.Properties.Core`
 open import Data.Nat.Properties public
   using (≤-pred)
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index b0a0eafcd6..f2755c55fc 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -62,6 +62,15 @@ m < n = suc m ≤ n
 pattern z<s {n}         = s≤s (z≤n {n})
 pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
 
+-- Smart destructors of _≤_, _<_
+
+s≤s⁻¹ : ∀ {m n} → suc m ≤ suc n → m ≤ n
+s≤s⁻¹ (s≤s m≤n) = m≤n
+
+s<s⁻¹ : ∀ {m n} → suc m < suc n → m < n
+s<s⁻¹ (s<s m<n) = m<n
+
+
 ------------------------------------------------------------------------
 -- other ordering relations
 
@@ -283,10 +292,10 @@ zero  ! = 1
 suc n ! = suc n * n !
 
 ------------------------------------------------------------------------
--- Alternative definition of _≤_
+-- Extensionally equivalent alternative definitions of _≤_/_<_ etc.
 
--- The following definition of _≤_ is more suitable for well-founded
--- induction (see Data.Nat.Induction)
+-- _≤′_: this definition is more suitable for well-founded induction
+-- (see Data.Nat.Induction)
 
 infix 4 _≤′_ _<′_ _≥′_ _>′_
 
@@ -308,8 +317,9 @@ m ≥′ n = n ≤′ m
 _>′_ : Rel ℕ 0ℓ
 m >′ n = n <′ m
 
-------------------------------------------------------------------------
--- Another alternative definition of _≤_
+-- _≤″_: this definition of _≤_ is used for proof-irrelevant ‵DivMod`
+-- and is a specialised instance of a general algebraic construction
+
 infix 4 _≤″_ _<″_ _≥″_ _>″_
 
 _≤″_ : (m n : ℕ)  → Set
@@ -326,10 +336,20 @@ m ≥″ n = n ≤″ m
 _>″_ : Rel ℕ 0ℓ
 m >″ n = n <″ m
 
-------------------------------------------------------------------------
--- Another alternative definition of _≤_
+-- Smart constructors of _≤″_ and _<″_
+
+pattern ≤″-offset k = less-than-or-equal {k = k} refl
+pattern <″-offset k = ≤″-offset k
+
+-- Smart destructors of _<″_
+
+s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
+s≤″s⁻¹ (≤″-offset k) = ≤″-offset k
+
+s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
+s<″s⁻¹ (<″-offset k) = <″-offset k
 
--- Useful for induction when you have an upper bound.
+-- _≤‴_: this definition is useful for induction with an upper bound.
 
 data _≤‴_ : ℕ → ℕ → Set where
   ≤‴-refl : ∀{m} → m ≤‴ m
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 638482131f..6109106b26 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -15,7 +15,7 @@ open import Algebra.Consequences.Propositional
 open import Data.Bool.Base using (if_then_else_; Bool; true; false)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Binary.Base
-open import Data.Nat as ℕ using (ℕ; z≤n; s≤s)
+open import Data.Nat as ℕ using (ℕ; z≤n; s≤s; s<s⁻¹)
 open import Data.Nat.DivMod using (_%_; _/_; m/n≤m; +-distrib-/-∣ˡ)
 open import Data.Nat.Divisibility using (∣-refl)
 import Data.Nat.Base as ℕᵇ
@@ -317,17 +317,17 @@ toℕ-cancel-< : ∀ {x y} → toℕ x ℕ.< toℕ y → x < y
 toℕ-cancel-< {zero}     {2[1+ y ]} x<y = 0<even
 toℕ-cancel-< {zero}     {1+[2 y ]} x<y = 0<odd
 toℕ-cancel-< {2[1+ x ]} {2[1+ y ]} x<y =
-  even<even (toℕ-cancel-< (ℕ.≤-pred (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
+  even<even (toℕ-cancel-< (s<s⁻¹ (ℕₚ.*-cancelˡ-< 2 _ _ x<y)))
 toℕ-cancel-< {2[1+ x ]} {1+[2 y ]} x<y
   rewrite ℕₚ.*-distribˡ-+ 2 1 (toℕ x) =
-  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (ℕₚ.≤-pred x<y))))
+  even<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕₚ.≤-trans (s≤s (ℕₚ.n≤1+n _)) (s<s⁻¹ x<y))))
 toℕ-cancel-< {1+[2 x ]} {2[1+ y ]} x<y with toℕ x ℕₚ.≟ toℕ y
 ... | yes x≡y = odd<even (inj₂ (toℕ-injective x≡y))
 ... | no  x≢y
   rewrite ℕₚ.+-suc (toℕ y) (toℕ y ℕ.+ 0) =
   odd<even (inj₁ (toℕ-cancel-< (ℕₚ.≤∧≢⇒< (ℕₚ.*-cancelˡ-≤ 2 (ℕₚ.+-cancelˡ-≤ 2 _ _ x<y)) x≢y)))
 toℕ-cancel-< {1+[2 x ]} {1+[2 y ]} x<y =
-  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (ℕ.≤-pred x<y)))
+  odd<odd (toℕ-cancel-< (ℕₚ.*-cancelˡ-< 2 _ _ (s<s⁻¹ x<y)))
 
 fromℕ-cancel-< : ∀ {x y} → fromℕ x < fromℕ y → x ℕ.< y
 fromℕ-cancel-< = subst₂ ℕ._<_ (toℕ-fromℕ _) (toℕ-fromℕ _) ∘ toℕ-mono-<
@@ -1459,7 +1459,7 @@ pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
 pred-mono-≤ {x} {y} x≤y = begin
   pred x             ≡⟨ cong pred (sym (fromℕ-toℕ x)) ⟩
   pred (fromℕ m)     ≡⟨ sym (fromℕ-pred m) ⟩
-  fromℕ (ℕ.pred m)   ≤⟨ fromℕ-mono-≤ (ℕₚ.pred-mono (toℕ-mono-≤ x≤y)) ⟩
+  fromℕ (ℕ.pred m)   ≤⟨ fromℕ-mono-≤ (ℕₚ.pred-mono-≤ (toℕ-mono-≤ x≤y)) ⟩
   fromℕ (ℕ.pred n)   ≡⟨ fromℕ-pred n ⟩
   pred (fromℕ n)     ≡⟨ cong pred (fromℕ-toℕ y) ⟩
   pred y             ∎
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index ad46644442..dbe99a30e6 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -20,7 +20,6 @@ open import Data.Nat.Properties
 open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (False; toWitnessFalse)
 
 open ≤-Reasoning
 
@@ -465,12 +464,13 @@ _div_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
 _div_ = _/_
 
 _mod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → Fin divisor
-m mod n@(suc _) = fromℕ< (m%n<n m n)
+m mod n = fromℕ< (m%n<n m n)
 
 _divMod_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} →
            DivMod dividend divisor
-m divMod n@(suc _) = result (m / n) (m mod n) (begin-equality
-  m                                   ≡⟨  m≡m%n+[m/n]*n m n ⟩
-  m % n                    + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< (m%n<n m n)) ⟩
-  toℕ (fromℕ< (m%n<n m n)) + [m/n]*n  ∎)
-  where [m/n]*n = m / n * n
+m divMod n = result (m / n) (m mod n) $ begin-equality
+  m                               ≡⟨  m≡m%n+[m/n]*n m n ⟩
+  m % n                + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ< [m%n]<n) ⟩
+  toℕ (fromℕ< [m%n]<n) + [m/n]*n  ∎
+  where [m/n]*n = m / n * n ; [m%n]<n = m%n<n m n
+
diff --git a/src/Data/Nat/DivMod/WithK.agda b/src/Data/Nat/DivMod/WithK.agda
index 458a7eef33..3f6047df60 100644
--- a/src/Data/Nat/DivMod/WithK.agda
+++ b/src/Data/Nat/DivMod/WithK.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.DivMod.WithK where
 
-open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_)
+open import Data.Nat using (ℕ; NonZero; _+_; _*_)
 open import Data.Nat.DivMod hiding (_mod_; _divMod_)
 open import Data.Nat.Properties using (≤⇒≤″)
 open import Data.Nat.WithK
@@ -16,7 +16,7 @@ open import Data.Fin.Base using (Fin; toℕ; fromℕ<″)
 open import Data.Fin.Properties using (toℕ-fromℕ<″)
 open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
-  using (refl; sym; cong; module ≡-Reasoning)
+  using (cong; module ≡-Reasoning)
 open import Relation.Binary.PropositionalEquality.WithK
 
 open ≡-Reasoning
@@ -27,17 +27,15 @@ infixl 7 _mod_ _divMod_
 -- Certified modulus
 
 _mod_ : (dividend divisor : ℕ) → .{{ _ : NonZero divisor }} → Fin divisor
-a mod n = fromℕ<″ (a % n) (≤″-erase (≤⇒≤″ (m%n<n a n)))
+m mod n = fromℕ<″ (m % n) (≤″-erase (≤⇒≤″ (m%n<n m n)))
 
 ------------------------------------------------------------------------
 -- Returns modulus and division result with correctness proof
 
 _divMod_ : (dividend divisor : ℕ) → .{{ NonZero divisor }} →
            DivMod dividend divisor
-a divMod n = result (a / n) (a mod n) $ ≡-erase $ begin
-  a                                 ≡⟨ m≡m%n+[m/n]*n a n ⟩
-  a % n              + [a/n]*n      ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ<″ lemma′)) ⟩
-  toℕ (fromℕ<″ _ lemma′) + [a/n]*n  ∎
-  where
-  lemma′ = ≤″-erase (≤⇒≤″ (m%n<n a n))
-  [a/n]*n = a / n * n
+m divMod n = result (m / n) (m mod n) $ ≡-erase $ begin
+  m                                 ≡⟨ m≡m%n+[m/n]*n m n ⟩
+  m % n                  + [m/n]*n  ≡˘⟨ cong (_+ [m/n]*n) (toℕ-fromℕ<″ lemma″) ⟩
+  toℕ (fromℕ<″ _ lemma″) + [m/n]*n  ∎
+  where [m/n]*n = m / n * n ; lemma″ = ≤″-erase (≤⇒≤″ (m%n<n m n))
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index cf6e2ab0cd..dcc6746f93 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -42,7 +42,7 @@ open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
 open import Algebra.Definitions {A = ℕ} _≡_
@@ -173,9 +173,7 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≤-total : Total _≤_
 ≤-total zero    _       = inj₁ z≤n
 ≤-total _       zero    = inj₂ z≤n
-≤-total (suc m) (suc n) with ≤-total m n
-... | inj₁ m≤n = inj₁ (s≤s m≤n)
-... | inj₂ n≤m = inj₂ (s≤s n≤m)
+≤-total (suc m) (suc n) = Sum.map s≤s s≤s (≤-total m n)
 
 ≤-irrelevant : Irrelevant _≤_
 ≤-irrelevant z≤n        z≤n        = refl
@@ -265,7 +263,7 @@ s≤s-injective : {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
 ≤-pred : suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
+≤-pred = s≤s⁻¹
 
 m≤n⇒m≤1+n : m ≤ n → m ≤ 1 + n
 m≤n⇒m≤1+n z≤n       = z≤n
@@ -427,7 +425,7 @@ s<s-injective : {p q : m < n} → s<s p ≡ s<s q → p ≡ q
 s<s-injective refl = refl
 
 <-pred : suc m < suc n → m < n
-<-pred (s<s m<n) = m<n
+<-pred = s<s⁻¹
 
 m<n⇒m<1+n : m < n → m < 1 + n
 m<n⇒m<1+n z<s               = z<s
@@ -464,12 +462,10 @@ m<n⇒n≢0 (s≤s m≤n) ()
 m<n⇒m≤1+n : m < n → m ≤ suc n
 m<n⇒m≤1+n = m≤n⇒m≤1+n ∘ <⇒≤
 
-m<1+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<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) = Sum.map s<s (cong suc) (m<1+n⇒m<n∨m≡n m<1+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)
@@ -717,7 +713,7 @@ 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) (s≤s m+1+n≤m) = m+1+n≰m m m+1+n≤m
+m+1+n≰m (suc m) m+1+n≤m = m+1+n≰m m (s≤s⁻¹ m+1+n≤m)
 
 m<m+n : ∀ m {n} → n > 0 → m < m + n
 m<m+n zero    n>0 = n>0
@@ -727,8 +723,8 @@ 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) (m<n⇒m<1+n m+n<n)
+m+n≮n zero    n                = n≮n n
+m+n≮n (suc m) n@(suc _) sm+n<n = m+n≮n m n (m<n⇒m<1+n (s<s⁻¹ sm+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)
@@ -1691,9 +1687,6 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
 -- Properties of pred
 ------------------------------------------------------------------------
 
-pred-mono : pred Preserves _≤_ ⟶ _≤_
-pred-mono m≤n = ∸-mono m≤n (≤-refl {1})
-
 pred[n]≤n : pred n ≤ n
 pred[n]≤n {zero}  = z≤n
 pred[n]≤n {suc n} = n≤1+n n
@@ -1712,6 +1705,13 @@ pred[n]≤n {suc n} = n≤1+n n
 suc-pred : ∀ n .{{_ : NonZero n}} → suc (pred n) ≡ n
 suc-pred (suc n) = refl
 
+pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
+pred-mono-≤ {zero}          _   = z≤n
+pred-mono-≤ {suc _} {suc _} m≤n = s≤s⁻¹ m≤n
+
+pred-mono-< : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+pred-mono-< {m = suc _} {n = suc _} = s<s⁻¹
+
 ------------------------------------------------------------------------
 -- Properties of ∣_-_∣
 ------------------------------------------------------------------------
@@ -2067,8 +2067,8 @@ m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
 <ᵇ⇒<″ : T (m <ᵇ n) → m <″ n
 <ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))
 
-<″⇒<ᵇ : m <″ n → T (m <ᵇ n)
-<″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)
+<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
+<″⇒<ᵇ {m} (<″-offset k) = <⇒<ᵇ (m≤m+n (suc m) k)
 
 -- equivalence to the old definition of _≤″_
 
@@ -2078,9 +2078,8 @@ m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)
 -- equivalence to _≤_
 
 ≤″⇒≤ : _≤″_ ⇒ _≤_
-≤″⇒≤ {zero}  (less-than-or-equal refl) = z≤n
-≤″⇒≤ {suc m} (less-than-or-equal refl) =
-  s≤s (≤″⇒≤ (less-than-or-equal refl))
+≤″⇒≤ {zero}  (≤″-offset k) = z≤n {k}
+≤″⇒≤ {suc m} (≤″-offset k) = s≤s (≤″⇒≤ (≤″-offset k))
 
 ≤⇒≤″ : _≤_ ⇒ _≤″_
 ≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n
@@ -2097,7 +2096,7 @@ _<″?_ : Decidable _<″_
 m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n))
 
 _≤″?_ : Decidable _≤″_
-zero  ≤″? n = yes (less-than-or-equal refl)
+zero  ≤″? n = yes (≤″-offset n)
 suc m ≤″? n = m <″? n
 
 _≥″?_ : Decidable _≥″_
@@ -2332,6 +2331,11 @@ suc[pred[n]]≡n {suc n} _   = refl
 "Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
 #-}
 
+pred-mono = pred-mono-≤
+{-# WARNING_ON_USAGE pred-mono
+"Warning: pred-mono was deprecated in v2.0. Please use pred-mono-≤ instead. "
+#-}
+
 {- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
 open Data.Nat.Base public
   using (*-rawMagma; *-1-rawMonoid)
diff --git a/src/Data/Nat/Properties/Core.agda b/src/Data/Nat/Properties/Core.agda
index 94031fdc37..66bfdaa32b 100644
--- a/src/Data/Nat/Properties/Core.agda
+++ b/src/Data/Nat/Properties/Core.agda
@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED. Please use
--- `Data.Nat.Properties` directly.
+-- `Data.Nat.Base directly.
 --
 ------------------------------------------------------------------------
 
@@ -12,7 +12,7 @@ module Data.Nat.Properties.Core where
 
 {-# WARNING_ON_IMPORT
 "Data.Nat.Properties.Core was deprecated in v2.0.
-Use Data.Nat.Properties instead."
+Use Data.Nat.Base instead."
 #-}
 
 open import Data.Nat.Base
@@ -22,4 +22,4 @@ open import Data.Nat.Base
 ------------------------------------------------------------------------
 
 ≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
+≤-pred = s≤s⁻¹
diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index 564264946c..13dd34ace2 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -6,21 +6,25 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Digit using (showDigit; toDigits)
 open import Data.Digit.Properties using (toDigits-injective; showDigit-injective)
-open import Function.Base using (_∘_)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
+open import Data.Nat.Show using (charsInBase)
+open import Function.Base using (_∘_)
 open import Relation.Nullary.Decidable using (True)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
-open import Data.Nat.Show using (charsInBase)
 
 module Data.Nat.Show.Properties where
 
 module _ (base : ℕ) {base≥2 : True (2 ≤? base)} {base≤16 : True (base ≤? 16)} where
 
-  charsInBase-injective : ∀ n m → charsInBase base {base≥2} {base≤16} n ≡ charsInBase base {base≥2} {base≤16} m → n ≡ m
-  charsInBase-injective n m = toDigits-injective base {base≥2} _ _
+  private
+    charsInBase-base         = charsInBase base {base≥2} {base≤16}
+    toDigits-injective-base  = toDigits-injective base {base≥2} {base≥2}
+    showDigit-injective-base = showDigit-injective base {base≤16} {base≤16}
+
+  charsInBase-injective : ∀ n m →  charsInBase-base n ≡ charsInBase-base m → n ≡ m
+  charsInBase-injective n m = toDigits-injective-base _ _
                             ∘ Listₚ.reverse-injective
-                            ∘ Listₚ.map-injective (showDigit-injective _ _ _)
+                            ∘ Listₚ.map-injective (showDigit-injective-base _ _)
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 0f56c9fbd7..1ecf91b9e7 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -8,7 +8,7 @@
 
 module Data.Vec.Base where
 
-open import Data.Bool.Base using (Bool; true; false; if_then_else_)
+open import Data.Bool.Base using (Bool; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda
index c857ee6642..63649e940e 100644
--- a/src/Data/Vec/Bounded/Base.agda
+++ b/src/Data/Vec/Bounded/Base.agda
@@ -131,12 +131,12 @@ align = alignWith id
 take : ∀ {m} n → Vec≤ A m → Vec≤ A (n ⊓ m)
 take             zero    _                = []
 take             (suc n) (Vec.[] , p)     = []
-take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , ℕₚ.≤-pred p)
+take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , s≤s⁻¹ p)
 
 drop : ∀ {m} n → Vec≤ A m → Vec≤ A (m ∸ n)
 drop             zero    v                = v
 drop             (suc n) (Vec.[] , p)     = []
-drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , ℕₚ.≤-pred p)
+drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , s≤s⁻¹ p)
 
 ------------------------------------------------------------------------
 -- Lifting a collection of bounded vectors to the same size
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 27df432105..38793a9038 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -31,7 +31,7 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′)
+open import Relation.Nullary.Decidable.Core using (Dec; does; yes; _×-dec_; map′)
 open import Relation.Nullary.Negation.Core using (contradiction)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
@@ -483,14 +483,14 @@ cast-++ʳ {m = suc m} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq 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    z<s       = refl
-lookup-++-< (x ∷ xs) ys (suc i) (s<s i<m) = lookup-++-< xs ys i i<m
+lookup-++-< (x ∷ xs) ys zero    _     = refl
+lookup-++-< (x ∷ xs) ys (suc i) si<sm = lookup-++-< xs ys i (s<s⁻¹ si<sm)
 
 lookup-++-≥ : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i≥m : toℕ i ≥ m) →
               lookup (xs ++ ys) i ≡ lookup ys (Fin.reduce≥ i i≥m)
-lookup-++-≥ []       ys i       i≥m       = refl
-lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m
+lookup-++-≥ []       ys i       _     = refl
+lookup-++-≥ (x ∷ xs) ys (suc i) si≥sm = lookup-++-≥ xs ys i (s≤s⁻¹ si≥sm)
 
 lookup-++ˡ : ∀ (xs : Vec A m) (ys : Vec A n) i →
              lookup (xs ++ ys) (i ↑ˡ n) ≡ lookup xs i
@@ -1396,7 +1396,7 @@ Please use take-map instead."
 drop-distr-zipWith = drop-zipWith
 {-# WARNING_ON_USAGE drop-distr-zipWith
 "Warning: drop-distr-zipWith was deprecated in v2.0.
-Please use tdrop-zipWith instead."
+Please use drop-zipWith instead."
 #-}
 drop-distr-map = drop-map
 {-# WARNING_ON_USAGE drop-distr-map
@@ -1441,7 +1441,7 @@ lookup-inject≤-take m m≤m+n i xs = sym (begin
   lookup (take m xs) i
     ≡⟨ lookup-take-inject≤ xs i ⟩
   lookup xs (Fin.inject≤ i _)
-    ≡⟨ cong ((lookup xs) ∘ (Fin.inject≤ i)) (≤-irrelevant _ _) ⟩
+    ≡⟨⟩
   lookup xs (Fin.inject≤ i m≤m+n)
     ∎) where open ≡-Reasoning
 {-# WARNING_ON_USAGE lookup-inject≤-take
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index c32e4c8df6..8ff5a4d2e3 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -8,23 +8,18 @@
 
 module Data.Vec.Relation.Unary.Linked.Properties where
 
-open import Data.Bool.Base using (true; false)
 open import Data.Vec.Base as Vec
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 import Data.Vec.Relation.Unary.All.Properties as Allₚ
 open import Data.Vec.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
 open import Data.Fin.Base using (zero; suc; _<_)
-open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
-open import Data.Nat.Properties using (<-pred)
+open import Data.Nat.Base using (ℕ; zero; suc; s<s⁻¹)
 open import Level using (Level)
-open import Function.Base using (_∘_; flip; _on_)
+open import Function.Base using (_on_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Transitive)
-open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (yes; no; does)
 
 private
   variable
@@ -49,7 +44,7 @@ module _ (trans : Transitive R) where
            Linked R xs → i < j →
            R (lookup xs i) (lookup xs j)
   lookup⁺ {i = zero}  {j = suc j} (rx ∷ rxs) i<j = Allₚ.lookup⁺ (Linked⇒All rx rxs) j
-  lookup⁺ {i = suc i} {j = suc j} (_  ∷ rxs) i<j = lookup⁺ rxs (<-pred i<j)
+  lookup⁺ {i = suc i} {j = suc j} (_  ∷ rxs) i<j = lookup⁺ rxs (s<s⁻¹ i<j)
 
 ------------------------------------------------------------------------
 -- Introduction (⁺) and elimination (⁻) rules for vec operations