resolves issue #1800: deprecates ≤-step etc. throughout

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

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₁

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))
 

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."

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)

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,15 +739,15 @@ 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)
   filter-some {x ∷ xs} (here px)   with P? x
   ... | 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
 
 ------------------------------------------------------------------------
 -- _ʳ++_

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

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₁))
 

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 →

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)

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 _)

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 _ _)

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

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)