Remove redundant cancel property.

It is in the standard library as `⁻¹-injective`.

6 files changed, 4 insertions, 16 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
index a6cbcab..cad9714 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
@@ -61,7 +61,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
 
   ; ⁻¹-anti-mono-<; ⁻¹-anti-mono-≤
 
-  ; ⁻¹-cancel; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤
+  ; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤
 
   ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε
   ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
index d303c99..aa265c8 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
 
   ; -‿anti-mono-<; -‿anti-mono-≤
-  ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤
+  ; -‿anti-cancel-<; -‿anti-cancel-≤
 
   ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
   ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index f9f0376..4531605 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
 
   ; -‿anti-mono-<; -‿anti-mono-≤
-  ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤
+  ; -‿anti-cancel-<; -‿anti-cancel-≤
 
   ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
   ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
index 1914a31..337947a 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -59,7 +59,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
   ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
 
   ; -‿anti-mono-<; -‿anti-mono-≤
-  ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤
+  ; -‿anti-cancel-<; -‿anti-cancel-≤
 
   ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
   ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
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 _<_ _>_ _⁻¹
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
index 5e51e89..eff2d37 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -102,7 +102,6 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian
   ; ⁻¹-anti-mono-< to -‿anti-mono-<
   ; ⁻¹-anti-mono-≤ to -‿anti-mono-≤
 
-  ; ⁻¹-cancel        to -‿cancel
   ; ⁻¹-anti-cancel-< to -‿anti-cancel-<
   ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤