Be a bit lazier

agda · Jan 30, 2025 · a8224d2 · a8224d2
1 parent d8d2001
commit a8224d2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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