From 038d2109e78d9c688acfc3338140cc908151db76 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 5 Apr 2022 12:08:00 +0100
Subject: Generalise 0 comparison to ≤.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda')

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
index aa37d59..7972c4f 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
@@ -72,4 +72,5 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
   ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε
 
   ; x<y⇒ε<y∙x⁻¹ ; ε<y∙x⁻¹⇒x<y
+  ; x≤y⇒ε≤y∙x⁻¹ ; ε≤y∙x⁻¹⇒x≤y
   )
-- 
cgit v1.2.3