diff --git a/CHANGELOG.md b/CHANGELOG.md
index c2433a4b1d..905e469c2d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1007,6 +1007,8 @@ Other minor changes
   combine-surjective : ∀ x → ∃₂ λ y z → combine y z ≡ x
 
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
+
+  i<1+i              : i < suc i
   ```
 
 * Added new functions in `Data.Integer.Base`:
@@ -1069,6 +1071,16 @@ Other minor changes
   ∷ʳ-++ : xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
   ```
 
+* Added new patterns and definitions to `Data.Nat.Base`:
+  ```agda
+  pattern z<s {n}         = s≤s (z≤n {n})
+  pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+
+  pattern <′-base          = ≤′-refl
+  pattern <′-step {n} m<′n = ≤′-step {n} m<′n
+  ```
+
+
 * Added new definitions and proofs to `Data.Nat.Primality`:
   ```agda
   Composite        : ℕ → Set
@@ -1091,6 +1103,17 @@ Other minor changes
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
+  ≤-pred        : suc m ≤ suc n → m ≤ n
+  s<s-injective : ∀ {p q : m < n} → s<s p ≡ s<s q → p ≡ q
+  <-pred        : suc m < suc n → m < n
+  <-step        : m < n → m < 1 + n
+  m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
+
+  z<′s : zero <′ suc n
+  s<′s : m <′ n → suc m <′ suc n
+  <⇒<′ : m < n → m <′ n
+  <′⇒< : m <′ n → m < n
+
   1≤n!    : 1 ≤ n !
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 9d2d04155f..ae1fd5809f 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1949,7 +1949,7 @@ s<′s (<′-step m<′n) = <′-step (s<′s m<′n)
 <′⇒< <′-base        = n<1+n _
 <′⇒< (<′-step m<′n) = <-step (<′⇒< m<′n)
 
-m<1+n⇒m<n∨m≡n′ :  ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
+m<1+n⇒m<n∨m≡n′ : ∀ {m n} → m < suc n → m < n ⊎ m ≡ n
 m<1+n⇒m<n∨m≡n′ m<n with <⇒<′ m<n
 ... | <′-base      = inj₂ refl
 ... | <′-step m<′n = inj₁ (<′⇒< m<′n)