Proof that pred is right adjoint to suc on ℕ._≤_

CHANGELOG.md

@@ -44,6 +44,12 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* New lemmas in `Data.Nat.Properties`: adjunction between `suc` and `pred`
+  ```agda
+  sm≤n⇒m≤pn : suc m ≤ n → m ≤ pred n
+  m≤pn⇒sm≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
+  ```
+
 * New lemma in `Data.Vec.Properties`:
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)

src/Data/Nat/Properties.agda

@@ -272,8 +272,14 @@ _≥?_ = flip _≤?_
 s≤s-injective : {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
 s≤s-injective refl = refl
 
+sm≤n⇒m≤pn : suc m ≤ n → m ≤ pred n
+sm≤n⇒m≤pn {n = suc _} = s≤s⁻¹
+
+m≤pn⇒sm≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
+m≤pn⇒sm≤n {n = suc _} = s≤s
+
 ≤-pred : suc m ≤ suc n → m ≤ n
-≤-pred = s≤s⁻¹
+≤-pred = sm≤n⇒m≤pn
 
 m≤n⇒m≤1+n : m ≤ n → m ≤ 1 + n
 m≤n⇒m≤1+n z≤n       = z≤n