Minor clean up.

1 files changed, 5 insertions, 5 deletions

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              ∎