From 2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sat, 2 Apr 2022 11:41:51 +0100
Subject: Add more properties for ordered structures.

---
 .../StrictTotal/Properties/AbelianGroup.agda       | 60 ++++++++++++++++++----
 1 file changed, 51 insertions(+), 9 deletions(-)

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

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
index fe64b32..a6cbcab 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
@@ -14,18 +14,60 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup
   where
 
 open AbelianGroup abelianGroup
-
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
 open import Relation.Binary.Core
 open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
 
 open import Algebra.Properties.AbelianGroup Unordered.abelianGroup public
 open import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised Unordered.commutativeMonoid public
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
 open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
-  using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>; x<y⇒ε<yx⁻¹)
-
-⁻¹-anti-mono : _⁻¹ Preserves _<_ ⟶ _>_
-⁻¹-anti-mono {x} {y} x<y = begin-strict
-  y ⁻¹            ≈˘⟨ identityˡ (y ⁻¹) ⟩
-  ε ∙ y ⁻¹        <⟨  ∙-invariantʳ (y ⁻¹) (x<y⇒ε<yx⁻¹ x<y) ⟩
-  y ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨  xyx⁻¹≈y y (x ⁻¹) ⟩
-  x ⁻¹            ∎
+  using
+  ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
+  ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
+
+  ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
+  ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
+  -- _∙_ pres signs
+  ; x≥ε∧y>ε⇒x∙y>ε; x>ε∧y≥ε⇒x∙y>ε
+  ; x≤ε∧y<ε⇒x∙y<ε; x<ε∧y≤ε⇒x∙y<ε
+  ; x≥ε∧y≥ε⇒x∙y≥ε; x≤ε∧y≤ε⇒x∙y≤ε
+  -- _∙_ resp signs
+  ; x≤ε∧x∙y>ε⇒y>ε; x≤ε∧y∙x>ε⇒y>ε
+  ; x<ε∧x∙y≥ε⇒y>ε; x<ε∧y∙x≥ε⇒y>ε
+  ; x≥ε∧x∙y<ε⇒y<ε; x≥ε∧y∙x<ε⇒y<ε
+  ; x>ε∧x∙y≤ε⇒y<ε; x>ε∧y∙x≤ε⇒y<ε
+  ; x≤ε∧x∙y≥ε⇒y≥ε; x≤ε∧y∙x≥ε⇒y≥ε
+  ; x≥ε∧x∙y≤ε⇒y≤ε; x≥ε∧y∙x≤ε⇒y≤ε
+
+  ; ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
+
+  ; n≢0⇒×-monoˡ-<; x>ε⇒×-monoʳ-<; x<ε⇒×-anti-monoʳ-<
+  ; ×-monoˡ-≤; x≥ε⇒×-monoʳ-≤; x≤ε⇒×-anti-monoʳ-≤
+
+  ; ×-cancelˡ-<; x≥ε⇒×-cancelʳ-<; x≤ε⇒×-anti-cancelʳ-<
+  ; n≢0⇒×-cancelˡ-≤; x>ε⇒×-cancelʳ-≤; x<ε⇒×-anti-cancelʳ-≤
+  -- _×_ pres signs
+  ; n≢0∧x>ε⇒n×x>ε; n≢0∧x<ε⇒n×x<ε
+  ; x≥ε⇒n×x≥ε; x≤ε⇒n×x≤ε
+  -- _×_ resp signs
+  ; n×x>ε⇒x>ε; n×x<ε⇒x<ε
+  ; n≢0∧n×x≥ε⇒x≥ε; n≢0∧n×x≤ε⇒x≤ε
+
+  ; ⁻¹-anti-mono-<; ⁻¹-anti-mono-≤
+
+  ; ⁻¹-cancel; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤
+
+  ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε
+  ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε
+
+  ; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε
+  ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε
+
+  ; x<y⇒ε<y∙x⁻¹ ; ε<y∙x⁻¹⇒x<y
+  )
-- 
cgit v1.2.3