From 0da5ba7629ca1a911958f155fbecf2cc85646c4a Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Thu, 15 Aug 2024 04:25:34 +0200
Subject: [PATCH] =?UTF-8?q?Proof=20that=20`pred`=20is=20right=20adjoint=20?=
 =?UTF-8?q?to=20`suc`=20on=20`=E2=84=95.=5F=E2=89=A4=5F`=20(#2456)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* prove that `pred` is right adjoint to `suc`

* add converse lemma for `NonZero n`

* add converse lemma for `NonZero n`

* rename lemmas
---
 CHANGELOG.md                 | 6 ++++++
 src/Data/Nat/Properties.agda | 8 +++++++-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8091cbfff9..9ae126acd4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -65,6 +65,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
+  suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
+  m≤pred[n]⇒suc[m]≤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)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 21ea925467..9911e2b9a1 100644
--- a/src/Data/Nat/Properties.agda
+++ b/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
 
+suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
+suc[m]≤n⇒m≤pred[n] {n = suc _} = s≤s⁻¹
+
+m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
+m≤pred[n]⇒suc[m]≤n {n = suc _} = s≤s
+
 ≤-pred : suc m ≤ suc n → m ≤ n
-≤-pred = s≤s⁻¹
+≤-pred = suc[m]≤n⇒m≤pred[n]
 
 m≤n⇒m≤1+n : m ≤ n → m ≤ 1 + n
 m≤n⇒m≤1+n z≤n       = z≤n