From b212c150ec0a9bf45cf6c28fba997693669e78d2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 5 Apr 2022 12:06:33 +0100
Subject: Minor clean up.

---
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(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 e186c71..5cf2d5b 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -202,14 +202,14 @@ x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x⁻¹
 x<y⇒ε<y∙x⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹
 x<y⇒ε<y∙x⁻¹ {x} {y} x<y = begin-strict
   ε        ≈˘⟨ inverseʳ x ⟩
-  x ∙ x ⁻¹ <⟨  ∙-invariantʳ (x ⁻¹) x<y ⟩
+  x ∙ x ⁻¹ <⟨  ∙-monoʳ-< x<y ⟩
   y ∙ x ⁻¹ ∎
 
 ε<y∙x⁻¹⇒x<y : ∀ {x y} → ε < y ∙ x ⁻¹ → x < y
 ε<y∙x⁻¹⇒x<y {x} {y} ε<yx⁻¹ = begin-strict
   x              ≈˘⟨ identityˡ x ⟩
-  ε ∙ x          <⟨ ∙-invariantʳ x ε<yx⁻¹ ⟩
-  y ∙ x ⁻¹ ∙ x   ≈⟨ assoc y (x ⁻¹) x ⟩
-  y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩
-  y ∙ ε          ≈⟨ identityʳ y ⟩
+  ε ∙ x          <⟨  ∙-monoʳ-< ε<yx⁻¹ ⟩
+  y ∙ x ⁻¹ ∙ x   ≈⟨  assoc y (x ⁻¹) x ⟩
+  y ∙ (x ⁻¹ ∙ x) ≈⟨  ∙-congˡ (inverseˡ x) ⟩
+  y ∙ ε          ≈⟨  identityʳ y ⟩
   y              ∎
-- 
cgit v1.2.3