Add ≤‴-irrelevant to Data.Nat.Properties (#2503)

* Add `≤‴-irrelevant` to `Data.Nat.Properties`

* Add <‴-irrefl and refactor using cong

* Minor simplifications

* Add to CHANGELOG

CHANGELOG.md

@@ -322,6 +322,11 @@ Additions to existing modules
   ```agda
   m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
   m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
+  <‴-irrefl : Irreflexive _≡_ _<‴_
+  ≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
+  <‴-irrelevant : Irrelevant {A = ℕ} _<‴_
+  >‴-irrelevant : Irrelevant {A = ℕ} _>‴_
+  ≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
   ```
 
   adjunction between `suc` and `pred`

src/Data/Nat/Properties.agda

@@ -2237,6 +2237,27 @@ _>‴?_ = flip _<‴?_
 ≤‴⇒≤ : _≤‴_ ⇒ _≤_
 ≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″
 
+<‴-irrefl : Irreflexive _≡_ _<‴_
+<‴-irrefl eq = <-irrefl eq ∘ ≤‴⇒≤
+
+≤‴-irrelevant : Irrelevant {A = ℕ} _≤‴_
+≤‴-irrelevant ≤‴-refl = lemma refl
+  where
+  lemma : ∀ {m n} → (e : m ≡ n) → (q : m ≤‴ n) → subst (m ≤‴_) e ≤‴-refl ≡ q
+  lemma {m} e    ≤‴-refl       = cong (λ e → subst (m ≤‴_) e ≤‴-refl) $ ≡-irrelevant e refl
+  lemma     refl (≤‴-step m<m) with () ← <‴-irrefl refl m<m
+≤‴-irrelevant (≤‴-step m<m) ≤‴-refl     with () ← <‴-irrefl refl m<m
+≤‴-irrelevant (≤‴-step p)   (≤‴-step q) = cong ≤‴-step $ ≤‴-irrelevant p q
+
+<‴-irrelevant : Irrelevant {A = ℕ} _<‴_
+<‴-irrelevant = ≤‴-irrelevant
+
+>‴-irrelevant : Irrelevant {A = ℕ} _>‴_
+>‴-irrelevant = ≤‴-irrelevant
+
+≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
+≥‴-irrelevant = ≤‴-irrelevant
+
 ------------------------------------------------------------------------
 -- Other properties
 ------------------------------------------------------------------------