diff --git a/CHANGELOG.md b/CHANGELOG.md
index 78dea52440..26b29feae3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -826,17 +826,23 @@ Deprecated names
   been made consistent so that `m`, `n` always refer to naturals and
   `i` and `j` always refer to integers:
   ```
+  ≤-steps        ↦  i≤j⇒i≤k+j
+  ≤-step         ↦  i≤j⇒i≤1+j
+
+  ≤-steps-neg    ↦  i≤j⇒i-k≤j
+  ≤-step-neg     ↦  i≤j⇒pred[i]≤j
+
   n≮n            ↦  i≮i
-  ∣n∣≡0⇒n≡0      ↦  ∣i∣≡0⇒i≡0
-  ∣-n∣≡∣n∣       ↦  ∣-i∣≡∣i∣
-  0≤n⇒+∣n∣≡n     ↦  0≤i⇒+∣i∣≡i
-  +∣n∣≡n⇒0≤n     ↦  +∣i∣≡i⇒0≤i
-  +∣n∣≡n⊎+∣n∣≡-n ↦  +∣i∣≡i⊎+∣i∣≡-i
-  ∣m+n∣≤∣m∣+∣n∣  ↦  ∣i+j∣≤∣i∣+∣j∣
-  ∣m-n∣≤∣m∣+∣n∣  ↦  ∣i-j∣≤∣i∣+∣j∣
-  signₙ◃∣n∣≡n    ↦  signᵢ◃∣i∣≡i
+  ∣n∣≡0⇒n≡0       ↦  ∣i∣≡0⇒i≡0
+  ∣-n∣≡∣n∣         ↦  ∣-i∣≡∣i∣
+  0≤n⇒+∣n∣≡n      ↦  0≤i⇒+∣i∣≡i
+  +∣n∣≡n⇒0≤n      ↦  +∣i∣≡i⇒0≤i
+  +∣n∣≡n⊎+∣n∣≡-n   ↦  +∣i∣≡i⊎+∣i∣≡-i
+  ∣m+n∣≤∣m∣+∣n∣     ↦  ∣i+j∣≤∣i∣+∣j∣
+  ∣m-n∣≤∣m∣+∣n∣     ↦  ∣i-j∣≤∣i∣+∣j∣
+  signₙ◃∣n∣≡n     ↦  signᵢ◃∣i∣≡i
   ◃-≡            ↦  ◃-cong
-  ∣m-n∣≡∣n-m∣    ↦  ∣i-j∣≡∣j-i∣
+  ∣m-n∣≡∣n-m∣      ↦  ∣i-j∣≡∣j-i∣
   m≡n⇒m-n≡0      ↦  i≡j⇒i-j≡0
   m-n≡0⇒m≡n      ↦  i-j≡0⇒i≡j
   m≤n⇒m-n≤0      ↦  i≤j⇒i-j≤0
@@ -849,7 +855,7 @@ Deprecated names
   m<n⇒m≤pred[n]  ↦  i<j⇒i≤pred[j]
   -1*n≡-n        ↦  -1*i≡-i
   m*n≡0⇒m≡0∨n≡0  ↦  i*j≡0⇒i≡0∨j≡0
-  ∣m*n∣≡∣m∣*∣n∣  ↦  ∣i*j∣≡∣i∣*∣j∣
+  ∣m*n∣≡∣m∣*∣n∣     ↦  ∣i*j∣≡∣i∣*∣j∣
   m≤m+n          ↦  i≤i+j
   n≤m+n          ↦  i≤j+i
   m-n≤m          ↦  i≤i-j
@@ -934,6 +940,10 @@ Deprecated names
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
+  ≤-step          ↦  m≤n⇒m≤1+n
+  ≤-stepsˡ        ↦  m≤n⇒m≤o+n
+  ≤-stepsʳ        ↦  m≤n⇒m≤n+o
+  <-step          ↦  m<n⇒m<1+n
   ```
 
 * In `Data.Rational.Unnormalised.Properties`:
@@ -942,6 +952,7 @@ Deprecated names
   ↧[p/q]≡q         ↦  ↧[n/d]≡d
   *-monoˡ-≤-pos    ↦  *-monoˡ-≤-nonNeg
   *-monoʳ-≤-pos    ↦  *-monoʳ-≤-nonNeg
+  ≤-steps          ↦  p≤q⇒p≤r+q
   *-monoˡ-≤-neg    ↦  *-monoˡ-≤-nonPos
   *-monoʳ-≤-neg    ↦  *-monoʳ-≤-nonPos
   *-cancelˡ-<-pos  ↦  *-cancelˡ-<-nonNeg
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 8a23d5049e..46e146c8c9 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -163,7 +163,7 @@ toℕ≤pred[n] zero                 = z≤n
 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 = ℕₚ.≤-step (toℕ≤pred[n] i)
+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)
@@ -471,7 +471,7 @@ inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 
 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 (ℕₚ.≤-step (subst (toℕ i ℕ.≤_) (toℕ-inject₁ j) i≤j))
+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))
 
 ------------------------------------------------------------------------
 -- lower₁
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 0dfaf2a578..a2863f672a 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -254,7 +254,7 @@ module _ (n : ℕ) where
 p⊆q⇒∣p∣≤∣q∣ : p ⊆ q → ∣ p ∣ ≤ ∣ q ∣
 p⊆q⇒∣p∣≤∣q∣ {p = []}          {[]}          p⊆q = z≤n
 p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {outside ∷ q} p⊆q = p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q)
-p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ℕₚ.≤-step (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
+p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ℕₚ.m≤n⇒m≤1+n (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
 p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {outside ∷ q} p⊆q = contradiction (p⊆q here) λ()
 p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {inside  ∷ q} p⊆q = s≤s (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
 
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 58f9aae16c..fa313d91f0 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -1034,11 +1034,11 @@ neg-distrib-+ -[1+ m ]  (+   n)   =
   n + j ∎
   where open ≤-Reasoning
 
-≤-steps : ∀ k .{{_ : NonNegative k}} → i ≤ j → i ≤ k + j
-≤-steps (+ n) i≤j = subst (_≤ _) (+-identityˡ _) (+-mono-≤ (+≤+ z≤n) i≤j)
+i≤j⇒i≤k+j : ∀ k .{{_ : NonNegative k}} → i ≤ j → i ≤ k + j
+i≤j⇒i≤k+j (+ n) i≤j = subst (_≤ _) (+-identityˡ _) (+-mono-≤ (+≤+ z≤n) i≤j)
 
 i≤j+i : ∀ i j .{{_ : NonNegative j}} → i ≤ j + i
-i≤j+i i j = ≤-steps j ≤-refl
+i≤j+i i j = i≤j⇒i≤k+j j ≤-refl
 
 i≤i+j : ∀ i j .{{_ : NonNegative j}} → i ≤ i + j
 i≤i+j i j rewrite +-comm i j = i≤j+i i j
@@ -1142,16 +1142,16 @@ i-j≡0⇒i≡j i j i-j≡0 = begin
   0ℤ + j        ≡⟨  +-identityˡ j ⟩
   j             ∎ where open ≡-Reasoning
 
-≤-steps-neg : ∀ k .{{_ : NonNegative k}} → i ≤ j → i - k ≤ j
-≤-steps-neg {i}         +0       i≤j rewrite +-identityʳ i = i≤j
-≤-steps-neg {+ m}       +[1+ n ] i≤j = ≤-trans (m⊖n≤m m (suc n)) i≤j
-≤-steps-neg { -[1+ m ]} +[1+ n ] i≤j = ≤-trans (-≤- (ℕ.≤-trans (ℕ.m≤m+n m n) (ℕ.n≤1+n _))) i≤j
+i≤j⇒i-k≤j : ∀ k .{{_ : NonNegative k}} → i ≤ j → i - k ≤ j
+i≤j⇒i-k≤j {i}         +0       i≤j rewrite +-identityʳ i = i≤j
+i≤j⇒i-k≤j {+ m}       +[1+ n ] i≤j = ≤-trans (m⊖n≤m m (suc n)) i≤j
+i≤j⇒i-k≤j { -[1+ m ]} +[1+ n ] i≤j = ≤-trans (-≤- (ℕ.≤-trans (ℕ.m≤m+n m n) (ℕ.n≤1+n _))) i≤j
 
 i-j≤i : ∀ i j .{{_ : NonNegative j}} → i - j ≤ i
-i-j≤i i j = ≤-steps-neg j ≤-refl
+i-j≤i i j = i≤j⇒i-k≤j j ≤-refl
 
 i≤j⇒i-j≤0 : i ≤ j → i - j ≤ 0ℤ
-i≤j⇒i-j≤0 {_}         {j}         -≤+       = ≤-steps-neg j -≤+
+i≤j⇒i-j≤0 {_}         {j}         -≤+       = i≤j⇒i-k≤j j -≤+
 i≤j⇒i-j≤0 { -[1+ m ]} { -[1+ n ]} (-≤- n≤m) = begin
   suc n ⊖ suc m ≡⟨ [1+m]⊖[1+n]≡m⊖n n m ⟩
   n ⊖ m         ≤⟨ ⊖-monoʳ-≥-≤ n n≤m ⟩
@@ -1196,11 +1196,11 @@ i≤j⇒0≤j-i {i} {j} i≤j = begin
 -- Properties of suc
 ------------------------------------------------------------------------
 
-≤-step : i ≤ j → i ≤ sucℤ j
-≤-step = ≤-steps (+ 1)
+i≤j⇒i≤1+j : i ≤ j → i ≤ sucℤ j
+i≤j⇒i≤1+j = i≤j⇒i≤k+j (+ 1)
 
 i≤suc[i] : ∀ i → i ≤ sucℤ i
-i≤suc[i] i = ≤-steps (+ 1) ≤-refl
+i≤suc[i] i = i≤j+i i (+ 1)
 
 suc-+ : ∀ m n → +[1+ m ] + n ≡ sucℤ (+ m + n)
 suc-+ m (+ n)      = refl
@@ -1285,11 +1285,11 @@ 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 ]} (-<- n<m) = -≤- n<m
 
-≤-step-neg : i ≤ j → pred i ≤ j
-≤-step-neg -≤+               = -≤+
-≤-step-neg (-≤- n≤m)         = -≤- (ℕ.≤-step n≤m)
-≤-step-neg (+≤+ z≤n)         = -≤+
-≤-step-neg (+≤+ (s≤s m≤n)) = +≤+ (ℕ.≤-step m≤n)
+i≤j⇒pred[i]≤j : i ≤ j → pred i ≤ j
+i≤j⇒pred[i]≤j -≤+               = -≤+
+i≤j⇒pred[i]≤j (-≤- n≤m)         = -≤- (ℕ.m≤n⇒m≤1+n n≤m)
+i≤j⇒pred[i]≤j (+≤+ z≤n)         = -≤+
+i≤j⇒pred[i]≤j (+≤+ (s≤s m≤n)) = +≤+ (ℕ.m≤n⇒m≤1+n m≤n)
 
 pred-mono : pred Preserves _≤_ ⟶ _≤_
 pred-mono (-≤+ {n = 0})     = -≤- z≤n
@@ -2252,6 +2252,26 @@ m-n≡0⇒m≡n = i-j≡0⇒i≡j
 "Warning: m-n≡0⇒m≡n was deprecated in v2.0
 Please use i-j≡0⇒i≡j instead."
 #-}
+≤-steps = i≤j⇒i≤k+j
+{-# WARNING_ON_USAGE ≤-steps
+"Warning: ≤-steps was deprecated in v2.0
+Please use i≤j⇒i≤k+j instead."
+#-}
+≤-steps-neg = i≤j⇒i-k≤j
+{-# WARNING_ON_USAGE ≤-steps-neg
+"Warning: ≤-steps-neg was deprecated in v2.0
+Please use i≤j⇒i-k≤j instead."
+#-}
+≤-step = i≤j⇒i≤1+j
+{-# WARNING_ON_USAGE ≤-step
+"Warning: ≤-step was deprecated in v2.0
+Please use i≤j⇒i≤1+j instead."
+#-}
+≤-step-neg = i≤j⇒pred[i]≤j
+{-# WARNING_ON_USAGE ≤-step-neg
+"Warning: ≤-step-neg was deprecated in v2.0
+Please use i≤j⇒pred[i]≤j instead."
+#-}
 m≤n⇒m-n≤0 = i≤j⇒i-j≤0
 {-# WARNING_ON_USAGE m≤n⇒m-n≤0
 "Warning: m≤n⇒m-n≤0 was deprecated in v2.0
@@ -2308,19 +2328,19 @@ Please use i*j≡0⇒i≡0∨j≡0 instead."
 Please use ∣i*j∣≡∣i∣*∣j∣ instead."
 #-}
 n≤m+n : ∀ n → i ≤ + n + i
-n≤m+n {i} n = ≤-steps (+ n) ≤-refl
+n≤m+n {i} n = i≤j+i i (+ n)
 {-# WARNING_ON_USAGE n≤m+n
 "Warning: n≤m+n was deprecated in v2.0
 Please use i≤j+i instead. Note the change of form of the explicit arguments."
 #-}
 m≤m+n : ∀ n → i ≤ i + + n
-m≤m+n {i} n rewrite +-comm i (+ n) = i≤j+i i (+ n)
+m≤m+n {i} n = i≤i+j i (+ n)
 {-# WARNING_ON_USAGE m≤m+n
 "Warning: m≤m+n was deprecated in v2.0
 Please use i≤i+j instead. Note the change of form of the explicit arguments."
 #-}
 m-n≤m : ∀ i n → i - + n ≤ i
-m-n≤m i n = ≤-steps-neg (+ n) ≤-refl
+m-n≤m i n = i-j≤i i (+ n)
 {-# WARNING_ON_USAGE m-n≤m
 "Warning: m-n≤m was deprecated in v2.0
 Please use i-j≤i instead. Note the change of form of the explicit arguments."
diff --git a/src/Data/List/Membership/Propositional/Properties.agda b/src/Data/List/Membership/Propositional/Properties.agda
index 133dc30b6d..985f92ecc9 100644
--- a/src/Data/List/Membership/Propositional/Properties.agda
+++ b/src/Data/List/Membership/Propositional/Properties.agda
@@ -361,7 +361,7 @@ finite inj (x ∷ xs) fᵢ∈x∷xs = excluded-middle helper
     ∈-if-not-i i≢j = not-x (i≢j ∘ f-inj ∘ trans fᵢ≡x ∘ sym)
 
     lemma : ∀ {k j} → i ≤ j → ¬ (i ≤ k) → suc j ≢ k
-    lemma i≤j i≰1+j refl = i≰1+j (≤-step i≤j)
+    lemma i≤j i≰1+j refl = i≰1+j (m≤n⇒m≤1+n i≤j)
 
     f′ⱼ∈xs : ∀ j → f′ j ∈ xs
     f′ⱼ∈xs j with i ≤ᵇ j | Reflects.invert (≤ᵇ-reflects-≤ i j)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 3a600acb4b..d9fef297c5 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -139,7 +139,7 @@ module _ (f : A → Maybe B) where
   length-mapMaybe []       = z≤n
   length-mapMaybe (x ∷ xs) with f x
   ... | just y  = s≤s (length-mapMaybe xs)
-  ... | nothing = ≤-step (length-mapMaybe xs)
+  ... | nothing = m≤n⇒m≤1+n (length-mapMaybe xs)
 
 ------------------------------------------------------------------------
 -- _++_
@@ -725,7 +725,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   length-filter : ∀ xs → length (filter P? xs) ≤ length xs
   length-filter []       = z≤n
   length-filter (x ∷ xs) with does (P? x)
-  ... | false = ≤-step (length-filter xs)
+  ... | false = m≤n⇒m≤1+n (length-filter xs)
   ... | true  = s≤s (length-filter xs)
 
   filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
@@ -739,7 +739,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | false because _ = s≤s (length-filter xs)
   ... | yes          px = contradiction px ¬px
   filter-notAll (x ∷ xs) (there any) with does (P? x)
-  ... | false = ≤-step (filter-notAll xs any)
+  ... | false = m≤n⇒m≤1+n (filter-notAll xs any)
   ... | true  = s≤s (filter-notAll xs any)
 
   filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
@@ -747,7 +747,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   ... | true because _ = z<s
   ... | no         ¬px = contradiction px ¬px
   filter-some {x ∷ xs} (there pxs) with does (P? x)
-  ... | true  = ≤-step (filter-some pxs)
+  ... | true  = m≤n⇒m≤1+n (filter-some pxs)
   ... | false = filter-some pxs
 
   filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
@@ -794,7 +794,7 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
   length-derun [] = ≤-refl
   length-derun (x ∷ []) = ≤-refl
   length-derun (x ∷ y ∷ xs) with does (R? x y) | length-derun (y ∷ xs)
-  ... | true  | r = ≤-step r
+  ... | true  | r = m≤n⇒m≤1+n r
   ... | false | r = s≤s r
 
   length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
@@ -832,8 +832,8 @@ module _ {P : Pred A p} (P? : Decidable P) where
                      length ys ≤ length xs × length zs ≤ length xs
   length-partition []       = z≤n , z≤n
   length-partition (x ∷ xs) with does (P? x) | length-partition xs
-  ...  | true  | rec = Prod.map s≤s ≤-step rec
-  ...  | false | rec = Prod.map ≤-step s≤s rec
+  ...  | true  | rec = Prod.map s≤s m≤n⇒m≤1+n rec
+  ...  | false | rec = Prod.map m≤n⇒m≤1+n s≤s rec
 
 ------------------------------------------------------------------------
 -- _ʳ++_
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index ee34828e36..48ebe35237 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -70,7 +70,7 @@ module _ {c t} {C : Set c} {T : REL A C t} where
 
 length-mono : ∀ {as bs} → Infix R as bs → length as ≤ length bs
 length-mono (here pref) = Prefixₚ.length-mono pref
-length-mono (there p)   = ℕₚ.≤-step (length-mono p)
+length-mono (there p)   = ℕₚ.m≤n⇒m≤1+n (length-mono p)
 
 ------------------------------------------------------------------------
 -- As an order
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 335894a701..01a286b2c5 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -115,8 +115,8 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 
 0<steps : ∀ {xs ys} (xs↭ys : xs ↭ ys) → 0 < steps xs↭ys
 0<steps (refl _)             = z<s
-0<steps (prep eq xs↭ys)      = ≤-step (0<steps xs↭ys)
-0<steps (swap eq₁ eq₂ xs↭ys) = ≤-step (0<steps xs↭ys)
+0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
+0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
 0<steps (trans xs↭ys xs↭ys₁) =
   <-transˡ (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index ea31331203..5fb04507cb 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -58,7 +58,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   length-mono-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs
   length-mono-≤ []        = z≤n
-  length-mono-≤ (y ∷ʳ rs) = ℕₚ.≤-step (length-mono-≤ rs)
+  length-mono-≤ (y ∷ʳ rs) = ℕₚ.m≤n⇒m≤1+n (length-mono-≤ rs)
   length-mono-≤ (r ∷ rs)  = s≤s (length-mono-≤ rs)
 
 ------------------------------------------------------------------------
@@ -219,7 +219,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
           Sublist R (drop m as) (drop n bs)
   drop⁺ {m} z≤n       rs        = drop-Sublist m rs
   drop⁺     (s≤s m≥n) []        = []
-  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.≤-step m≥n) rs
+  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.m≤n⇒m≤1+n m≥n) rs
   drop⁺     (s≤s m≥n) (r ∷ rs)  = drop⁺ m≥n rs
 
   drop⁺-≥ : ∀ {m n as bs} → m ≥ n → Pointwise R as bs →
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
index 36aa5259f6..669a08bc60 100644
--- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
@@ -76,7 +76,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   length-mono : ∀ {as bs} → Suffix R as bs → length as ≤ length bs
   length-mono (here rs)   = ≤-reflexive (Pointwise-length rs)
-  length-mono (there suf) = ≤-step (length-mono suf)
+  length-mono (there suf) = m≤n⇒m≤1+n (length-mono suf)
 
   S[as][bs]⇒∣as∣≢1+∣bs∣ : ∀ {as bs} → Suffix R as bs →
                           length as ≢ suc (length bs)
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 5b9cdb8871..32dbbc43b6 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -30,7 +30,7 @@ open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing)
 open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
-open import Data.Nat.Properties using (≤-refl; ≤-step)
+open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
 open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
@@ -543,7 +543,7 @@ all-upTo n = applyUpTo⁺₁ id n id
 
 applyDownFrom⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyDownFrom f n)
 applyDownFrom⁺₁ f zero    Pf = []
-applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ ≤-step)
+applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ m≤n⇒m≤1+n)
 
 applyDownFrom⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyDownFrom f n)
 applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _)
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index e9c0b84424..0a588cc0b1 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin)
 open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
-open import Data.Nat.Properties using (≤-refl; ≤-step)
+open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
 open import Function.Base using (_∘_; flip)
 open import Level using (Level)
 open import Relation.Binary using (Rel; DecSetoid)
@@ -104,7 +104,7 @@ module _ {R : Rel A ℓ} where
   applyDownFrom⁺₁ f zero    Rf = []
   applyDownFrom⁺₁ f (suc n) Rf =
     All.applyDownFrom⁺₁ _ n (flip Rf ≤-refl)  ∷
-    applyDownFrom⁺₁ f n (λ j<i i<n → Rf j<i (≤-step i<n))
+    applyDownFrom⁺₁ f n (λ j<i i<n → Rf j<i (m<n⇒m<1+n i<n))
 
   applyDownFrom⁺₂ : ∀ f n → (∀ i j → R (f i) (f j)) → AllPairs R (applyDownFrom f n)
   applyDownFrom⁺₂ f n Rf = applyDownFrom⁺₁ f n (λ _ _ → Rf _ _)
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index eac897890f..e5d96fe42b 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -22,7 +22,7 @@ open import Data.List.Membership.Propositional.Properties.Core
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
 open import Data.Nat using (zero; suc; _<_; z<s; s<s; s≤s)
-open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; ≤-step)
+open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1+n)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product as Prod
@@ -506,7 +506,7 @@ module _ {P : A → Set p} where
                    ∃ λ i → i < n × P (f i)
   applyDownFrom⁻ f {suc n} (here p)  = n , ≤-refl , p
   applyDownFrom⁻ f {suc n} (there p) with applyDownFrom⁻ f p
-  ... | i , i<n , pf = i , ≤-step i<n , pf
+  ... | i , i<n , pf = i , m<n⇒m<1+n i<n , pf
 
 ------------------------------------------------------------------------
 -- tabulate
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index d00b76a329..494e710f84 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; ≤-step)
+open import Data.Nat.Properties using (≤-refl; ≤-pred; 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)
@@ -116,7 +116,7 @@ module _ {R : Rel A ℓ} where
   applyDownFrom⁺₁ f zero          Rf = []
   applyDownFrom⁺₁ f (suc zero)    Rf = [-]
   applyDownFrom⁺₁ f (suc (suc n)) Rf =
-    Rf ≤-refl ∷ applyDownFrom⁺₁ f (suc n) (Rf ∘ ≤-step)
+    Rf ≤-refl ∷ applyDownFrom⁺₁ f (suc n) (Rf ∘ m≤n⇒m≤1+n)
 
   applyDownFrom⁺₂ : ∀ f n → (∀ i → R (f (suc i)) (f i)) →
                     Linked R (applyDownFrom f n)
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 6864f8cb09..d91e11c5b4 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -23,7 +23,7 @@ open import Data.Maybe.Base using (just)
 open import Relation.Nullary using (does)
 open import Data.Nat using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
-open import Data.Nat.Properties using (≤-step)
+open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product as Prod using (_,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary using (DecTotalOrder)
@@ -51,7 +51,7 @@ private
   length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
   length-mergePairs _ _ []              = s<s z<s
   length-mergePairs _ _ (xss ∷ [])      = s<s (s<s z<s)
-  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (≤-step (length-mergePairs xs ys xss))
+  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll []        _               = []
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 4271c62749..2f79568895 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -281,7 +281,7 @@ toℕ-mono-< {zero}     {2[1+ _ ]} _               =  ℕₚ.0<1+n
 toℕ-mono-< {zero}     {1+[2 _ ]} _               =  ℕₚ.0<1+n
 toℕ-mono-< {2[1+ x ]} {2[1+ y ]} (even<even x<y) =  begin
   ℕ.suc (2 ℕ.* (ℕ.suc xN))    ≤⟨ ℕₚ.+-monoʳ-≤ 1 (ℕₚ.*-monoʳ-≤ 2 xN<yN) ⟩
-  ℕ.suc (2 ℕ.* yN)            ≤⟨ ℕₚ.≤-step ℕₚ.≤-refl ⟩
+  ℕ.suc (2 ℕ.* yN)            ≤⟨ ℕₚ.n≤1+n _ ⟩
   2 ℕ.+ (2 ℕ.* yN)            ≡⟨ sym (ℕₚ.*-distribˡ-+ 2 1 yN) ⟩
   2 ℕ.* (ℕ.suc yN)            ∎
   where open ℕₚ.≤-Reasoning;  xN = toℕ x;  yN = toℕ y;  xN<yN = toℕ-mono-< x<y
@@ -291,7 +291,7 @@ toℕ-mono-< {1+[2 x ]} {2[1+ y ]} (odd<even (inj₁ x<y)) =   begin
   ℕ.suc (ℕ.suc (2 ℕ.* xN))    ≡⟨⟩
   2 ℕ.+ (2 ℕ.* xN)            ≡⟨ sym (ℕₚ.*-distribˡ-+ 2 1 xN) ⟩
   2 ℕ.* (ℕ.suc xN)            ≤⟨ ℕₚ.*-monoʳ-≤ 2 xN<yN ⟩
-  2 ℕ.* yN                    ≤⟨ ℕₚ.*-monoʳ-≤ 2 (ℕₚ.≤-step ℕₚ.≤-refl) ⟩
+  2 ℕ.* yN                    ≤⟨ ℕₚ.*-monoʳ-≤ 2 (ℕₚ.n≤1+n _) ⟩
   2 ℕ.* (ℕ.suc yN)            ∎
   where open ℕₚ.≤-Reasoning;  xN = toℕ x;  yN = toℕ y;  xN<yN = toℕ-mono-< x<y
 toℕ-mono-< {1+[2 x ]} {2[1+ .x ]} (odd<even (inj₂ refl)) =
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index d33c388608..d25cd7a3b2 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -255,12 +255,12 @@ 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)
+m≤n⇒m≤1+n : ∀ {m n} → m ≤ n → m ≤ 1 + n
+m≤n⇒m≤1+n z≤n       = z≤n
+m≤n⇒m≤1+n (s≤s m≤n) = s≤s (m≤n⇒m≤1+n m≤n)
 
 n≤1+n : ∀ n → n ≤ 1 + n
-n≤1+n _ = ≤-step ≤-refl
+n≤1+n _ = m≤n⇒m≤1+n ≤-refl
 
 1+n≰n : ∀ {n} → 1 + n ≰ n
 1+n≰n (s≤s 1+n≤n) = 1+n≰n 1+n≤n
@@ -417,9 +417,9 @@ 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)
+m<n⇒m<1+n : ∀ {m n} → m < n → m < 1 + n
+m<n⇒m<1+n z<s               = z<s
+m<n⇒m<1+n (s<s m<n@(s≤s _)) = s<s (m<n⇒m<1+n m<n)
 
 n≮0 : ∀ {n} → n ≮ 0
 n≮0 ()
@@ -450,7 +450,7 @@ m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
 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<n⇒m≤1+n = m≤n⇒m≤1+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
@@ -653,12 +653,12 @@ m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))
 +-cancel-< : Cancellative _<_ _+_
 +-cancel-< = +-cancelˡ-< , +-cancelʳ-<
 
-≤-stepsˡ : ∀ {m n} o → m ≤ n → m ≤ o + n
-≤-stepsˡ zero    m≤n = m≤n
-≤-stepsˡ (suc o) m≤n = ≤-step (≤-stepsˡ o m≤n)
+m≤n⇒m≤o+n : ∀ {m n} o → m ≤ n → m ≤ o + n
+m≤n⇒m≤o+n zero    m≤n = m≤n
+m≤n⇒m≤o+n (suc o) m≤n = m≤n⇒m≤1+n (m≤n⇒m≤o+n o m≤n)
 
-≤-stepsʳ : ∀ {m n} o → m ≤ n → m ≤ n + o
-≤-stepsʳ {m} o m≤n = subst (m ≤_) (+-comm o _) (≤-stepsˡ o m≤n)
+m≤n⇒m≤n+o : ∀ {m n} o → m ≤ n → m ≤ n + o
+m≤n⇒m≤n+o {m} o m≤n = subst (m ≤_) (+-comm o _) (m≤n⇒m≤o+n o m≤n)
 
 m≤m+n : ∀ m n → m ≤ m + n
 m≤m+n zero    n = z≤n
@@ -686,7 +686,7 @@ 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} z<s               o≤p = s≤s (≤-stepsˡ n o≤p)
++-mono-<-≤ {_} {suc n} z<s               o≤p = s≤s (m≤n⇒m≤o+n n o≤p)
 +-mono-<-≤ {_} {_}     (s<s m<n@(s≤s _)) o≤p = s≤s (+-mono-<-≤ m<n o≤p)
 
 +-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
@@ -715,7 +715,7 @@ 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) (m<n⇒m<1+n 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)
@@ -1534,7 +1534,7 @@ m>n⇒m∸n≢0 {n = suc n} (s≤s m>n) = m>n⇒m∸n≢0 m>n
 
 m≤n⇒n∸m≤n : ∀ {m n} → m ≤ n → n ∸ m ≤ n
 m≤n⇒n∸m≤n z≤n       = ≤-refl
-m≤n⇒n∸m≤n (s≤s m≤n) = ≤-step (m≤n⇒n∸m≤n m≤n)
+m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
 
 ---------------------------------------------------------------
 -- Properties of _∸_ and _+_
@@ -1663,7 +1663,7 @@ pred[n]≤n {suc n} = n≤1+n n
 
 ≤pred⇒≤ : ∀ {m n} → m ≤ pred n → m ≤ n
 ≤pred⇒≤ {m} {zero}  le = le
-≤pred⇒≤ {m} {suc n} le = ≤-step le
+≤pred⇒≤ {m} {suc n} le = m≤n⇒m≤1+n le
 
 ≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n
 ≤⇒pred≤ {zero}  le = le
@@ -1719,7 +1719,7 @@ m∸n≤∣m-n∣ m n with ≤-total m n
 ∣m-n∣≤m⊔n : ∀ m n → ∣ m - n ∣ ≤ m ⊔ n
 ∣m-n∣≤m⊔n zero    m       = ≤-refl
 ∣m-n∣≤m⊔n (suc m) zero    = ≤-refl
-∣m-n∣≤m⊔n (suc m) (suc n) = ≤-step (∣m-n∣≤m⊔n m n)
+∣m-n∣≤m⊔n (suc m) (suc n) = m≤n⇒m≤1+n (∣m-n∣≤m⊔n m n)
 
 ∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
 ∣-∣-identityˡ x = refl
@@ -1882,7 +1882,7 @@ m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
 ⌊n/2⌋≤n : ∀ n → ⌊ n /2⌋ ≤ n
 ⌊n/2⌋≤n zero          = z≤n
 ⌊n/2⌋≤n (suc zero)    = z≤n
-⌊n/2⌋≤n (suc (suc n)) = s≤s (≤-step (⌊n/2⌋≤n n))
+⌊n/2⌋≤n (suc (suc n)) = s≤s (m≤n⇒m≤1+n (⌊n/2⌋≤n n))
 
 ⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
 ⌊n/2⌋<n zero    = z<s
@@ -1937,7 +1937,7 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
 
 ≤′⇒≤ : _≤′_ ⇒ _≤_
 ≤′⇒≤ ≤′-refl        = ≤-refl
-≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)
+≤′⇒≤ (≤′-step m≤′n) = m≤n⇒m≤1+n (≤′⇒≤ m≤′n)
 
 ≤⇒≤′ : _≤_ ⇒ _≤′_
 ≤⇒≤′ z≤n       = z≤′n
@@ -1964,7 +1964,7 @@ s<′s (<′-step m<′n) = <′-step (s<′s m<′n)
 
 <′⇒< : ∀ {m n} → m <′ n → m < n
 <′⇒< <′-base        = n<1+n _
-<′⇒< (<′-step m<′n) = <-step (<′⇒< m<′n)
+<′⇒< (<′-step m<′n) = m<n⇒m<1+n (<′⇒< 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
@@ -2133,7 +2133,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   anyUpTo? zero    = no λ {(_ , () , _)}
   anyUpTo? (suc v) with P? v | anyUpTo? v
   ... | yes Pv | _                  = yes (v , ≤-refl , Pv)
-  ... | _      | yes (n , n<v , Pn) = yes (n , ≤-step n<v , Pn)
+  ... | _      | yes (n , n<v , Pn) = yes (n , m≤n⇒m≤1+n n<v , Pn)
   ... | no ¬Pv | no ¬Pn<v           = no ¬Pn<1+v
     where
     ¬Pn<1+v : ∄ λ n → n < suc v × P n
@@ -2145,7 +2145,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
   allUpTo? zero    = yes λ()
   allUpTo? (suc v) with P? v | allUpTo? v
   ... | no ¬Pv | _        = no (λ prf → ¬Pv   (prf ≤-refl))
-  ... | _      | no ¬Pn<v = no (λ prf → ¬Pn<v (prf ∘ ≤-step))
+  ... | _      | no ¬Pn<v = no (λ prf → ¬Pn<v (prf ∘ m≤n⇒m≤1+n))
   ... | yes Pn | yes Pn<v = yes Pn<1+v
     where
       Pn<1+v : ∀ {n} → n < suc v → P n
@@ -2259,3 +2259,23 @@ 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"
 #-}
+
+≤-step = m≤n⇒m≤1+n
+{-# WARNING_ON_USAGE ≤-step
+"Warning: ≤-step was deprecated in v2.0. Please use m≤n⇒m≤1+n instead. "
+#-}
+
+≤-stepsˡ = m≤n⇒m≤o+n
+{-# WARNING_ON_USAGE ≤-stepsˡ
+"Warning: ≤-stepsˡ was deprecated in v2.0. Please use m≤n⇒m≤o+n instead. "
+#-}
+
+≤-stepsʳ = m≤n⇒m≤n+o
+{-# WARNING_ON_USAGE ≤-stepsʳ
+"Warning: ≤-stepsʳ was deprecated in v2.0. Please use m≤n⇒m≤n+o instead. "
+#-}
+
+<-step = m<n⇒m<1+n
+{-# WARNING_ON_USAGE <-step
+"Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
+#-}
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 3e2118a301..5dc3d4d2bc 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -745,11 +745,11 @@ private
 +-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
 +-mono-≤ {p} {q} {u} {v} p≤q u≤v = ≤-trans (+-monoˡ-≤ u p≤q) (+-monoʳ-≤ q u≤v)
 
-≤-steps : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
-≤-steps {p} {q} r p≤q = subst (_≤ r + q) (+-identityˡ-≡ p) (+-mono-≤ (nonNegative⁻¹ r) p≤q)
+p≤q⇒p≤r+q : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
+p≤q⇒p≤r+q {p} {q} r p≤q = subst (_≤ r + q) (+-identityˡ-≡ p) (+-mono-≤ (nonNegative⁻¹ r) p≤q)
 
 p≤q+p : ∀ p q .{{_ : NonNegative q}} → p ≤ q + p
-p≤q+p p q = ≤-steps q ≤-refl
+p≤q+p p q = p≤q⇒p≤r+q q ≤-refl
 
 p≤p+q : ∀ p q .{{_ : NonNegative q}} → p ≤ p + q
 p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
@@ -1784,6 +1784,11 @@ Please use *-monoʳ-≤-nonNeg instead."
 "Warning: *-monoˡ-≤-nonNeg was deprecated in v2.0.
 Please use *-monoˡ-≤-nonNeg instead."
 #-}
+≤-steps = p≤q⇒p≤r+q
+{-# WARNING_ON_USAGE ≤-steps
+"Warning: ≤-steps was deprecated in v2.0
+Please use p≤q⇒p≤r+q instead."
+#-}
 *-monoˡ-≤-neg : ∀ r → Negative r → (_* r) Preserves _≤_ ⟶ _≥_
 *-monoˡ-≤-neg r@(mkℚᵘ -[1+ _ ] _) _ = *-monoˡ-≤-nonPos r
 {-# WARNING_ON_USAGE *-monoˡ-≤-neg
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 97d27767cb..805570c42e 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
 open import Data.Nat.Properties
-  using (+-assoc; ≤-step; ≤-refl; ≤-trans; suc-injective)
+  using (+-assoc; m≤n⇒m≤1+n; ≤-refl; ≤-trans; suc-injective)
 open import Data.Product as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -1055,7 +1055,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
   count≤n []       = z≤n
   count≤n (x ∷ xs) with does (P? x)
   ... | true  = s≤s (count≤n xs)
-  ... | false = ≤-step (count≤n xs)
+  ... | false = m≤n⇒m≤1+n (count≤n xs)
 
 ------------------------------------------------------------------------
 -- insert