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

---
 .../Algebra/Ordered/StrictTotal/Properties/Group.agda     | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
index 5cf2d5b..81c57ad 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -213,3 +213,18 @@ x<y⇒ε<y∙x⁻¹ {x} {y} x<y = begin-strict
   y ∙ (x ⁻¹ ∙ x) ≈⟨  ∙-congˡ (inverseˡ x) ⟩
   y ∙ ε          ≈⟨  identityʳ y ⟩
   y              ∎
+
+x≤y⇒ε≤y∙x⁻¹ : ∀ {x y} → x ≤ y → ε ≤ y ∙ x ⁻¹
+x≤y⇒ε≤y∙x⁻¹ {x} {y} x≤y = begin
+  ε        ≈˘⟨ inverseʳ x ⟩
+  x ∙ x ⁻¹ ≤⟨  ∙-monoʳ-≤ x≤y ⟩
+  y ∙ x ⁻¹ ∎
+
+ε≤y∙x⁻¹⇒x≤y : ∀ {x y} → ε ≤ y ∙ x ⁻¹ → x ≤ y
+ε≤y∙x⁻¹⇒x≤y {x} {y} ε≤y∙x⁻¹ = begin
+  x              ≈˘⟨ identityˡ x ⟩
+  ε ∙ x          ≤⟨  ∙-monoʳ-≤ ε≤y∙x⁻¹ ⟩
+  y ∙ x ⁻¹ ∙ x   ≈⟨  assoc y (x ⁻¹) x ⟩
+  y ∙ (x ⁻¹ ∙ x) ≈⟨  ∙-congˡ (inverseˡ x) ⟩
+  y ∙ ε          ≈⟨  identityʳ y ⟩
+  y              ∎
-- 
cgit v1.2.3