From a8224d2d2ccf5866278feea1ed3e5ed5397c9f87 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 30 Jan 2025 12:59:59 +0100
Subject: [PATCH] Be a bit lazier

---
 src/Data/Nat/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index e4b04f02be..20428045ea 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -205,8 +205,8 @@ _≥?_ = flip _≤?_
 
 ≤-total : Total _≤_
 ≤-total m n with m ≤? n
-... | yes m≤n = inj₁ m≤n
-... | no  m≰n = inj₂ (≰⇒≥ m≰n)
+... | true because m≤n = inj₁ (invert m≤n)
+... | false because m≰n = inj₂ (≰⇒≥ (invert m≰n))
 
 ------------------------------------------------------------------------
 -- Structures