From 9b3598fbdddd2bdaf43e094e9e16d62a0fc32d27 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Wed, 5 Feb 2025 13:28:46 -0800
Subject: [PATCH] Decide for natural numbers whether x<y or y<=x

---
 .../strict-inequality-natural-numbers.lagda.md           | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
index 1957d38b9d..dc859952a8 100644
--- a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
@@ -320,6 +320,15 @@ le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =
   le-leq-neq-ℕ {x} {y} l (λ p → f (ap succ-ℕ p))
 ```
 
+### For any two natural numbers `x` and `y`, either `x < y` or `y ≤ x`
+
+```agda
+decide-le-leq-ℕ : (x y : ℕ) → le-ℕ x y + leq-ℕ y x
+decide-le-leq-ℕ x zero-ℕ = inr star
+decide-le-leq-ℕ zero-ℕ (succ-ℕ _) = inl star
+decide-le-leq-ℕ (succ-ℕ x) (succ-ℕ y) = decide-le-leq-ℕ x y
+```
+
 ### If `1 < x` and `1 < y`, then `1 < xy`
 
 ```agda