1 files changed, 0 insertions, 11 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
index d72ae10..cf8e4f2 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -94,17 +94,6 @@ open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder
 
 ---- Cancellative
 
--- _≈_
-
-⁻¹-cancel : Injective _≈_ _≈_ _⁻¹
-⁻¹-cancel {x} {y} x⁻¹≈y⁻¹ = begin-equality
-  x       ≈⟨ inverseˡ-unique x (y ⁻¹) (begin-equality
-    x ∙ y ⁻¹ ≈˘⟨ ∙-congˡ x⁻¹≈y⁻¹ ⟩
-    x ∙ x ⁻¹ ≈⟨  inverseʳ x ⟩
-    ε        ∎) ⟩
-  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive y ⟩
-  y       ∎
-
 -- _<_
 
 ⁻¹-anti-cancel-< : Injective _<_ _>_ _⁻¹