Proof that pred is right adjoint to suc on ℕ._≤_ (#2456)

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

* add converse lemma for `NonZero n`

* add converse lemma for `NonZero n`

* rename lemmas

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)

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