Add more properties for ordered structures.

10 files changed, 1537 insertions, 129 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
index 831f591..0f8df22 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -30,19 +30,6 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     _<_     : Rel Carrier ℓ₂
     _∙_     : Op₂ Carrier
 
-  infix 4 _≉_ _≤_ _>_ _≥_
-  _≉_ : Rel Carrier _
-  x ≉ y = N.¬ x ≈ y
-
-  _≤_ : Rel Carrier _
-  x ≤ y = x < y ⊎ x ≈ y
-
-  _>_ : Rel Carrier _
-  _>_ = flip _<_
-
-  _≥_ : Rel Carrier _
-  _≥_ = flip _≤_
-
   module Unordered where
     rawMagma : NoOrder.RawMagma c ℓ₁
     rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ }
@@ -63,9 +50,6 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   rawMagma : RawMagma _ _ _
   rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
 
-  open RawMagma rawMagma public
-    using (_≉_; _≤_; _>_; _≥_)
-
   module Unordered where
     magma : NoOrder.Magma c ℓ₁
     magma = record { isMagma = IsMagma.Unordered.isMagma isMagma }
@@ -92,7 +76,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   magma = record { isMagma = isMagma }
 
   open Magma magma public
-    using (_≉_; _≤_; _>_; _≥_; rawMagma)
+    using (rawMagma)
 
   module Unordered where
     semigroup : NoOrder.Semigroup c ℓ₁
@@ -117,9 +101,6 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   rawMagma : RawMagma c ℓ₁ ℓ₂
   rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ }
 
-  open RawMagma rawMagma public
-    using (_≉_; _≤_; _>_; _≥_)
-
   module Unordered where
     rawMonoid : NoOrder.RawMonoid c ℓ₁
     rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε }
@@ -145,7 +126,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   semigroup = record { isSemigroup = isSemigroup }
 
   open Semigroup semigroup public
-    using (_≉_; _≤_; _>_; _≥_; rawMagma; magma)
+    using (rawMagma; magma)
 
   rawMonoid : RawMonoid _ _ _
   rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε}
@@ -175,7 +156,7 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε }
 
   open RawMonoid rawMonoid public
-    using (_≉_; _≤_; _>_; _≥_; rawMagma)
+    using (rawMagma)
 
   module Unordered where
     rawGroup : NoOrder.RawGroup c ℓ₁
@@ -207,7 +188,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   monoid = record { isMonoid = isMonoid }
 
   open Monoid monoid public
-    using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid)
+    using (rawMagma; magma; semigroup; rawMonoid)
 
   module Unordered where
     group : NoOrder.Group c ℓ₁
@@ -239,8 +220,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
   open Group group public
     using
-    ( _≉_; _≤_; _>_; _≥_
-    ; magma; semigroup; monoid
+    ( magma; semigroup; monoid
     ; rawMagma; rawMonoid; rawGroup
     )
 
@@ -273,7 +253,7 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   +-rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _+_; ε = 0#; _⁻¹ = -_ }
 
   open RawGroup +-rawGroup public
-    using ( _≉_; _≤_; _>_; _≥_ )
+    using ()
     renaming
     ( rawMagma to +-rawMagma
     ; rawMonoid to +-rawMonoid
@@ -328,7 +308,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
 
   open AbelianGroup +-abelianGroup public
-    using ( _≉_; _≤_; _>_; _≥_ )
+    using ()
     renaming
     ( rawMagma to +-rawMagma
     ; rawMonoid to +-rawMonoid
@@ -388,8 +368,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
 
   open Ring ring public
     using
-    ( _≉_; _≤_; _>_; _≥_
-    ; rawRing
+    ( rawRing
     ; +-rawMagma; +-rawMonoid; +-rawGroup
     ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
     ; *-rawMagma; *-rawMonoid
@@ -447,8 +426,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
   open RawRing rawRing public
     using
-    ( _≉_; _≤_; _>_; _≥_
-    ; +-rawMagma; +-rawMonoid; +-rawGroup
+    ( +-rawMagma; +-rawMonoid; +-rawGroup
     ; *-rawMagma; *-rawMonoid
     )
 
@@ -514,8 +492,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
   open Ring ring public
     using
-    ( _≉_; _≤_; _>_; _≥_
-    ; rawRing
+    ( rawRing
     ; +-rawMagma; +-rawMonoid; +-rawGroup
     ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
     ; *-rawMagma; *-rawMonoid
@@ -570,8 +547,7 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
   open DivisionRing divisionRing public
     using
-    ( _≉_; _≤_; _>_; _≥_
-    ; rawRing; rawField; ring
+    ( rawRing; rawField; ring
     ; +-rawMagma; +-rawMonoid; +-rawGroup
     ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
     ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda b/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda
new file mode 100644
index 0000000..7696f98
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda
@@ -0,0 +1,137 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Relations between algebraic properties of ordered structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary
+
+module Helium.Algebra.Ordered.StrictTotal.Consequences
+  {a ℓ₁ ℓ₂}
+  (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open StrictTotalOrder strictTotalOrder
+  renaming
+  ( Carrier to A
+  ; trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+
+open import Algebra.Core
+open import Algebra.Definitions
+open import Data.Product using (_,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Function using (_∘_)
+open import Function.Definitions
+open import Helium.Algebra.Ordered.Definitions
+open import Relation.Nullary using (¬_)
+
+----
+-- Consequences for a single unary operation
+module _ {f : Op₁ A} where
+  cong₁+mono₁-<⇒mono₁-≤ : Congruent₁ _≈_ f → Congruent₁ _<_ f → Congruent₁ _≤_ f
+  cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₁ x<y) = inj₁ (mono x<y)
+  cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₂ x≈y) = inj₂ (cong x≈y)
+
+  cong₁+anti-mono₁-<⇒anti-mono₁-≤ : Congruent₁ _≈_ f → f Preserves _<_ ⟶ _>_ → f Preserves _≤_ ⟶ _≥_
+  cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₁ x<y) = inj₁ (anti-mono x<y)
+  cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₂ x≈y) = inj₂ (cong (Eq.sym x≈y))
+
+  mono₁-<⇒cancel₁-≤ : Congruent₁ _<_ f → Injective _≤_ _≤_ f
+  mono₁-<⇒cancel₁-≤ mono fx≤fy = ≮⇒≥ (≤⇒≯ fx≤fy ∘ mono)
+
+  mono₁-≤⇒cancel₁-< : Congruent₁ _≤_ f → Injective _<_ _<_ f
+  mono₁-≤⇒cancel₁-< mono fx<fy = ≰⇒> (<⇒≱ fx<fy ∘ mono)
+
+  cancel₁-<⇒mono₁-≤ : Injective _<_ _<_ f → Congruent₁ _≤_ f
+  cancel₁-<⇒mono₁-≤ cancel x≤y = ≮⇒≥ (≤⇒≯ x≤y ∘ cancel)
+
+  cancel₁-≤⇒mono₁-< : Injective _≤_ _≤_ f → Congruent₁ _<_ f
+  cancel₁-≤⇒mono₁-< cancel x<y = ≰⇒> (<⇒≱ x<y ∘ cancel)
+
+  anti-mono₁-<⇒anti-cancel₁-≤ : f Preserves _<_ ⟶ _>_ → Injective _≤_ _≥_ f
+  anti-mono₁-<⇒anti-cancel₁-≤ anti-mono fx≥fy = ≮⇒≥ (≤⇒≯ fx≥fy ∘ anti-mono)
+
+  anti-mono₁-≤⇒anti-cancel₁-< : f Preserves _≤_ ⟶ _≥_ → Injective _<_ _>_ f
+  anti-mono₁-≤⇒anti-cancel₁-< anti-mono fx>fy = ≰⇒> (<⇒≱ fx>fy ∘ anti-mono)
+
+  mono₁-<⇒cancel₁ : Congruent₁ _<_ f → Injective _≈_ _≈_ f
+  mono₁-<⇒cancel₁ mono fx≈fy = ≮∧≯⇒≈ (<-irrefl fx≈fy ∘ mono) (<-irrefl (Eq.sym fx≈fy) ∘ mono)
+
+  anti-mono₁-<⇒cancel₁ : f Preserves _<_ ⟶ _>_ → Injective _≈_ _≈_ f
+  anti-mono₁-<⇒cancel₁ anti-mono fx≈fy = ≮∧≯⇒≈
+    (<-irrefl (Eq.sym fx≈fy) ∘ anti-mono)
+    (<-irrefl fx≈fy ∘ anti-mono)
+
+----
+-- Consequences for a single binary operation
+module _ {_∙_ : Op₂ A} where
+  invariant⇒mono-< : Invariant _<_ _∙_ → Congruent₂ _<_ _∙_
+  invariant⇒mono-< (invˡ , invʳ) {x} {y} {u} {v} x<y u<v = begin-strict
+    x ∙ u <⟨ invˡ x u<v ⟩
+    x ∙ v <⟨ invʳ v x<y ⟩
+    y ∙ v ∎
+
+  invariantˡ⇒monoˡ-< : LeftInvariant _<_ _∙_ → LeftCongruent _<_ _∙_
+  invariantˡ⇒monoˡ-< invˡ u<v = invˡ _ u<v
+
+  invariantʳ⇒monoʳ-< : RightInvariant _<_ _∙_ → RightCongruent _<_ _∙_
+  invariantʳ⇒monoʳ-< invʳ x<y = invʳ _ x<y
+
+  cong+invariant⇒mono-≤ : Congruent₂ _≈_ _∙_ → Invariant _<_ _∙_ → Congruent₂ _≤_ _∙_
+  cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₁ u<v) = inj₁ (invariant⇒mono-< inv x<y u<v)
+  cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₂ u≈v) = inj₁ (<-respʳ-≈ (cong Eq.refl u≈v) (invʳ _ x<y))
+  cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₁ u<v) = inj₁ (<-respʳ-≈ (cong x≈y Eq.refl) (invˡ _ u<v))
+  cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₂ u≤v) = inj₂ (cong x≈y u≤v)
+
+  congˡ+monoˡ-<⇒monoˡ-≤ : LeftCongruent _≈_ _∙_ → LeftCongruent _<_ _∙_ → LeftCongruent _≤_ _∙_
+  congˡ+monoˡ-<⇒monoˡ-≤ congˡ monoˡ = cong₁+mono₁-<⇒mono₁-≤ congˡ monoˡ
+
+  congʳ+monoʳ-<⇒monoʳ-≤ : RightCongruent _≈_ _∙_ → RightCongruent _<_ _∙_ → RightCongruent _≤_ _∙_
+  congʳ+monoʳ-<⇒monoʳ-≤ congʳ monoʳ = cong₁+mono₁-<⇒mono₁-≤ congʳ monoʳ
+
+  monoˡ-<⇒cancelˡ-≤ : LeftCongruent _<_ _∙_ → LeftCancellative _≤_ _∙_
+  monoˡ-<⇒cancelˡ-≤ monoˡ _ = mono₁-<⇒cancel₁-≤ monoˡ
+
+  monoʳ-<⇒cancelʳ-≤ : RightCongruent _<_ _∙_ → RightCancellative _≤_ _∙_
+  monoʳ-<⇒cancelʳ-≤ monoʳ _ _ = mono₁-<⇒cancel₁-≤ monoʳ
+
+  monoˡ-≤⇒cancelˡ-< : LeftCongruent _≤_ _∙_ → LeftCancellative _<_ _∙_
+  monoˡ-≤⇒cancelˡ-< monoˡ _ = mono₁-≤⇒cancel₁-< monoˡ
+
+  monoʳ-≤⇒cancelʳ-< : RightCongruent _≤_ _∙_ → RightCancellative _<_ _∙_
+  monoʳ-≤⇒cancelʳ-< monoʳ _ _ = mono₁-≤⇒cancel₁-< monoʳ
+
+  cancelˡ-<⇒monoˡ-≤ : LeftCancellative _<_ _∙_ → LeftCongruent _≤_ _∙_
+  cancelˡ-<⇒monoˡ-≤ cancelˡ = cancel₁-<⇒mono₁-≤ (cancelˡ _)
+
+  cancelʳ-<⇒monoʳ-≤ : RightCancellative _<_ _∙_ → RightCongruent _≤_ _∙_
+  cancelʳ-<⇒monoʳ-≤ cancelʳ = cancel₁-<⇒mono₁-≤ (cancelʳ _ _)
+
+  cancelˡ-≤⇒monoˡ-< : LeftCancellative _≤_ _∙_ → LeftCongruent _<_ _∙_
+  cancelˡ-≤⇒monoˡ-< cancelˡ = cancel₁-≤⇒mono₁-< (cancelˡ _)
+
+  cancelʳ-≤⇒monoʳ-< : RightCancellative _≤_ _∙_ → RightCongruent _<_ _∙_
+  cancelʳ-≤⇒monoʳ-< cancelʳ = cancel₁-≤⇒mono₁-< (cancelʳ _ _)
+
+  monoˡ-<⇒cancelˡ : LeftCongruent _<_ _∙_ → LeftCancellative _≈_ _∙_
+  monoˡ-<⇒cancelˡ monoˡ _ = mono₁-<⇒cancel₁ monoˡ
+
+  monoʳ-<⇒cancelʳ : RightCongruent _<_ _∙_ → RightCancellative _≈_ _∙_
+  monoʳ-<⇒cancelʳ monoʳ _ _ = mono₁-<⇒cancel₁ monoʳ
+
+  ¬comm-< : A → ¬ Commutative _<_ _∙_
+  ¬comm-< a comm = <-irrefl Eq.refl (comm a a )
+
+  -- cong+mono-<⇒mono-≤ : Congruent₂ _≈_ _∙_ → Congruent₂ _<_ _∙_ → Congruent₂ _≤_ _∙_
+  -- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₁ u<v) = inj₁ (mono x<y u<v)
+  -- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₂ u≈v) = inj₁ {!!}
+  -- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₁ u<v) = inj₁ {!!}
+  -- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₂ u≈v) = inj₂ (cong x≈y u≈v)
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
new file mode 100644
index 0000000..dbce970
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
@@ -0,0 +1,98 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Morphisms for ordered algebraic structures.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Algebra.Ordered.StrictTotal.Morphism.Structures where
+
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Morphism.Structures
+
+private
+  variable
+    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
+
+module MagmaMorphisms (M₁ : RawMagma a ℓ₁ ℓ₂) (M₂ : RawMagma b ℓ₃ ℓ₄) where
+  private
+    module M₁ = RawMagma M₁
+    module M₂ = RawMagma M₂
+
+  open M₁ using () renaming (Carrier to A)
+  open M₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B M₂._≈_
+
+  record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isOrderHomomorphism : IsOrderHomomorphism M₁._≈_ M₂._≈_ M₁._<_ M₂._<_ ⟦_⟧
+      homo                : Homomorphic₂ ⟦_⟧ M₁._∙_ M₂._∙_
+
+    open IsOrderHomomorphism isOrderHomomorphism public
+
+module MonoidMorphisms (M₁ : RawMonoid a ℓ₁ ℓ₂) (M₂ : RawMonoid b ℓ₃ ℓ₄) where
+  private
+    module M₁ = RawMonoid M₁
+    module M₂ = RawMonoid M₂
+
+  open M₁ using () renaming (Carrier to A)
+  open M₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B M₂._≈_
+  open MagmaMorphisms M₁.rawMagma M₂.rawMagma
+
+  record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
+      ε-homo              : Homomorphic₀ ⟦_⟧ M₁.ε M₂.ε
+
+    open IsMagmaHomomorphism isMagmaHomomorphism public
+
+module GroupMorphisms (G₁ : RawGroup a ℓ₁ ℓ₂) (G₂ : RawGroup b ℓ₃ ℓ₄) where
+  private
+    module G₁ = RawGroup G₁
+    module G₂ = RawGroup G₂
+
+  open G₁ using () renaming (Carrier to A)
+  open G₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B G₂._≈_
+  open MonoidMorphisms G₁.rawMonoid G₂.rawMonoid
+
+  record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
+      ⁻¹-homo              : Homomorphic₁ ⟦_⟧ G₁._⁻¹ G₂._⁻¹
+
+    open IsMonoidHomomorphism isMonoidHomomorphism public
+
+module RingMorphisms (R₁ : RawRing a ℓ₁ ℓ₂) (R₂ : RawRing b ℓ₃ ℓ₄) where
+  private
+    module R₁ = RawRing R₁
+    module R₂ = RawRing R₂
+
+  open R₁ using () renaming (Carrier to A)
+  open R₂ using () renaming (Carrier to B)
+  open MorphismDefinitions A B R₂._≈_
+  open GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup
+
+  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
+    field
+      +-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
+      *-homo                : Homomorphic₂ ⟦_⟧ R₁._*_ R₂._*_
+      1#-homo               : Homomorphic₀ ⟦_⟧ R₁.1# R₂.1#
+
+    open IsGroupHomomorphism +-isGroupHomomorphism public
+      renaming
+      ( homo to +-homo
+      ; ε-homo to 0#-homo
+      ; ⁻¹-homo to -‿homo
+      ; isMagmaHomomorphism to +-isMagmaHomomorphism
+      ; isMonoidHomomorphism to +-isMonoidHomomorphism
+      )
+
+open MagmaMorphisms public
+open MonoidMorphisms public
+open GroupMorphisms public
+open RingMorphisms public
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
+  )
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
index 24b2663..d303c99 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -14,14 +14,87 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
   where
 
 open CommutativeRing commutativeRing
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
+  )
 
 open import Algebra.Properties.Ring Unordered.ring public
   renaming (-0#≈0# to -0≈0)
 open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
 open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
 open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   using
-  ( <⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>
-  ; x<y⇒0<y-x; -‿anti-mono
-  ; ⊤′; number; negative
-  ; 0≤1; 1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)
+  ( +-mono-<; +-monoˡ-<; +-monoʳ-<
+  ; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤
+
+  ; +-cancel-<; +-cancelˡ-<; +-cancelʳ-<
+  ; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤
+
+  ; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0
+  ; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0
+  ; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0
+
+  ; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0
+  ; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0
+  ; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0
+  ; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0
+
+  ; ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
+
+  ; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-<
+  ; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤
+
+  ; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-<
+  ; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤
+
+  ; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0
+  ; x≥0⇒n×x≥0; x≤0⇒n×x≤0
+
+  ; n×x>0⇒x>0; n×x<0⇒x<0
+  ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0
+
+  ; -‿anti-mono-<; -‿anti-mono-≤
+  ; -‿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
+
+  ; x<y⇒0<y-x; 0<y-x⇒x<y
+
+  ; 0≤1; 1≈0⇒x≈y; x<y⇒0<1
+
+  ; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-<
+  ; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤
+
+  ; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-<
+  ; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤
+
+  ; x≈0⇒x*y≈0; x≈0⇒y*x≈0
+
+  ; -x*-y≈x*y
+  ;                x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0
+  ; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0
+
+  ; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1
+  ; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1
+
+  ; x*x≥0
+
+  ; ^-zeroˡ; ^-zeroʳ
+  ; ^-identityʳ
+
+  ; n≢0⇒0^n≈0
+  ; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-<
+  ; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤
+
+  ; x>0⇒x^n>0
+  ; x≥0⇒x^n≥0
+
+  ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
+  ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
+  )
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
index c0723b3..d72ae10 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -14,46 +14,205 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.Group
   where
 
 open Group group
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
 
-open import Data.Sum using (inj₂; [_,_]′; fromInj₁)
-open import Function using (_∘_; flip)
-open import Relation.Binary using (tri<; tri≈; tri>)
+open import Algebra.Definitions
+open import Function using (_∘_; flip; Injective)
+open import Relation.Binary.Core
 open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
 
 open import Algebra.Properties.Group Unordered.group public
 open import Algebra.Properties.Monoid.Mult.TCOptimised Unordered.monoid public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Monoid monoid public
+  using
+  ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
+  ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
 
-<⇒≱ : ∀ {x y} → x < y → ¬ x ≥ y
-<⇒≱ {x} {y} x<y x≥y with compare x y
-... | tri< _   x≉y x≱y = [ x≱y , x≉y ∘ Eq.sym ]′ x≥y
-... | tri≈ x≮y _   _   = x≮y x<y
-... | tri> x≮y _   _   = x≮y x<y
+  ; ∙-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≤ε
 
-≤⇒≯ : ∀ {x y} → x ≤ y → ¬ x > y
-≤⇒≯ = flip <⇒≱
+  ; ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
 
->⇒≉ : ∀ {x y} → x > y → x ≉ y
->⇒≉ x>y = <⇒≱ x>y ∘ inj₂
+  ; n≢0⇒×-monoˡ-<; x>ε⇒×-monoʳ-<; x<ε⇒×-anti-monoʳ-<
+  ; ×-monoˡ-≤; x≥ε⇒×-monoʳ-≤; x≤ε⇒×-anti-monoʳ-≤
 
-≈⇒≯ : ∀ {x y} → x ≈ y → ¬ x > y
-≈⇒≯ = flip >⇒≉
+  ; ×-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≤ε
+  )
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
 
-<⇒≉ : ∀ {x y} → x < y → x ≉ y
-<⇒≉ x<y = >⇒≉ x<y ∘ Eq.sym
+--------------------------------------------------------------------------------
+---- Properties of _⁻¹
 
-≈⇒≮ : ∀ {x y} → x ≈ y → ¬ x < y
-≈⇒≮ = flip <⇒≉
+---- Congruences
 
-≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
-≤∧≉⇒< x≤y x≉y = fromInj₁ (λ x≈y → contradiction x≈y x≉y) x≤y
+-- _<_
 
-≥∧≉⇒> : ∀ {x y} → x ≥ y → x ≉ y → x > y
-≥∧≉⇒> x≥y x≉y = ≤∧≉⇒< x≥y (x≉y ∘ Eq.sym)
+⁻¹-anti-mono-< : _⁻¹ Preserves _<_ ⟶ _>_
+⁻¹-anti-mono-< {x} {y} x<y = begin-strict
+  y ⁻¹              ≈˘⟨ identityˡ (y ⁻¹) ⟩
+  ε ∙ y ⁻¹          ≈˘⟨ ∙-congʳ (inverseˡ x) ⟩
+  x ⁻¹ ∙ x ∙ y ⁻¹   <⟨  ∙-monoʳ-< (∙-monoˡ-< x<y) ⟩
+  x ⁻¹ ∙ y ∙ y ⁻¹   ≈⟨  assoc (x ⁻¹) y (y ⁻¹) ⟩
+  x ⁻¹ ∙ (y ∙ y ⁻¹) ≈⟨  ∙-congˡ (inverseʳ y) ⟩
+  x ⁻¹ ∙ ε          ≈⟨  identityʳ (x ⁻¹) ⟩
+  x ⁻¹              ∎
 
-x<y⇒ε<yx⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹
-x<y⇒ε<yx⁻¹ {x} {y} x<y = begin-strict
+-- _≤_
+
+⁻¹-anti-mono-≤ : _⁻¹ Preserves _≤_ ⟶ _≥_
+⁻¹-anti-mono-≤ {x} {y} x≤y = begin
+  y ⁻¹              ≈˘⟨ identityˡ (y ⁻¹) ⟩
+  ε ∙ y ⁻¹          ≈˘⟨ ∙-congʳ (inverseˡ x) ⟩
+  x ⁻¹ ∙ x ∙ y ⁻¹   ≤⟨  ∙-monoʳ-≤ (∙-monoˡ-≤ x≤y) ⟩
+  x ⁻¹ ∙ y ∙ y ⁻¹   ≈⟨  assoc (x ⁻¹) y (y ⁻¹) ⟩
+  x ⁻¹ ∙ (y ∙ y ⁻¹) ≈⟨  ∙-congˡ (inverseʳ y) ⟩
+  x ⁻¹ ∙ ε          ≈⟨  identityʳ (x ⁻¹) ⟩
+  x ⁻¹              ∎
+
+---- 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 _<_ _>_ _⁻¹
+⁻¹-anti-cancel-< x⁻¹>y⁻¹ = ≰⇒> (<⇒≱ x⁻¹>y⁻¹ ∘ ⁻¹-anti-mono-≤)
+
+-- _≤_
+
+⁻¹-anti-cancel-≤ : Injective _≤_ _≥_ _⁻¹
+⁻¹-anti-cancel-≤ x⁻¹≥y⁻¹ = ≮⇒≥ (≤⇒≯ x⁻¹≥y⁻¹ ∘ ⁻¹-anti-mono-<)
+
+---- Preserves signs
+
+-- _<_
+
+x<ε⇒x⁻¹>ε : ∀ {x} → x < ε → x ⁻¹ > ε
+x<ε⇒x⁻¹>ε {x} x<ε = begin-strict
+  ε    ≈˘⟨ ε⁻¹≈ε ⟩
+  ε ⁻¹ <⟨  ⁻¹-anti-mono-< x<ε ⟩
+  x ⁻¹ ∎
+
+x>ε⇒x⁻¹<ε : ∀ {x} → x > ε → x ⁻¹ < ε
+x>ε⇒x⁻¹<ε {x} x>ε = begin-strict
+  x ⁻¹ <⟨ ⁻¹-anti-mono-< x>ε ⟩
+  ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩
+  ε    ∎
+
+-- _≤_
+
+x≤ε⇒x⁻¹≥ε : ∀ {x} → x ≤ ε → x ⁻¹ ≥ ε
+x≤ε⇒x⁻¹≥ε {x} x≤ε = begin
+  ε    ≈˘⟨ ε⁻¹≈ε ⟩
+  ε ⁻¹ ≤⟨  ⁻¹-anti-mono-≤ x≤ε ⟩
+  x ⁻¹ ∎
+
+x≥ε⇒x⁻¹≤ε : ∀ {x} → x ≥ ε → x ⁻¹ ≤ ε
+x≥ε⇒x⁻¹≤ε {x} x≥ε = begin
+  x ⁻¹ ≤⟨ ⁻¹-anti-mono-≤ x≥ε ⟩
+  ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩
+  ε    ∎
+
+---- Respects signs
+
+-- _<_
+
+x⁻¹<ε⇒x>ε : ∀ {x} → x ⁻¹ < ε → x > ε
+x⁻¹<ε⇒x>ε {x} x⁻¹<ε = begin-strict
+  ε       <⟨ x<ε⇒x⁻¹>ε x⁻¹<ε ⟩
+  x ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive x ⟩
+  x       ∎
+
+x⁻¹>ε⇒x<ε : ∀ {x} → x ⁻¹ > ε → x < ε
+x⁻¹>ε⇒x<ε {x} x⁻¹>ε = begin-strict
+  x       ≈˘⟨ ⁻¹-involutive x ⟩
+  x ⁻¹ ⁻¹ <⟨  x>ε⇒x⁻¹<ε x⁻¹>ε ⟩
+  ε       ∎
+
+-- _≤_
+
+x⁻¹≤ε⇒x≥ε : ∀ {x} → x ⁻¹ ≤ ε → x ≥ ε
+x⁻¹≤ε⇒x≥ε {x} x⁻¹≤ε = begin
+  ε       ≤⟨ x≤ε⇒x⁻¹≥ε x⁻¹≤ε ⟩
+  x ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive x ⟩
+  x       ∎
+
+x⁻¹≥ε⇒x≤ε : ∀ {x} → x ⁻¹ ≥ ε → x ≤ ε
+x⁻¹≥ε⇒x≤ε {x} x⁻¹≥ε = begin
+  x       ≈˘⟨ ⁻¹-involutive x ⟩
+  x ⁻¹ ⁻¹ ≤⟨  x≥ε⇒x⁻¹≤ε x⁻¹≥ε ⟩
+  ε       ∎
+
+-- ---- Infer signs
+
+-- -- _≈_
+
+-- x⁻¹≈x⇒x≈ε : ∀ {x} → x ⁻¹ ≈ x → x ≈ ε
+-- x⁻¹≈x⇒x≈ε {x} x⁻¹≈x = ≮∧≯⇒≈
+--   (λ x<ε → <-asym x<ε (begin-strict
+--     ε    <⟨ x<ε⇒x⁻¹>ε x<ε ⟩
+--     x ⁻¹ ≈⟨ x⁻¹≈x ⟩
+--     x    ∎))
+--   (λ x>ε → <-asym x>ε (begin-strict
+--     x    ≈˘⟨ x⁻¹≈x ⟩
+--     x ⁻¹ <⟨  x>ε⇒x⁻¹<ε x>ε ⟩
+--     ε    ∎))
+
+-- -- _<_
+
+-- x⁻¹<x⇒x>ε : ∀ {x} → x ⁻¹ < x → x > ε
+-- x⁻¹<x⇒x>ε x⁻¹<x = ≰⇒> (<⇒≱ x⁻¹<x ∘ λ x≤ε → ≤-trans x≤ε (x≤ε⇒x⁻¹≥ε x≤ε))
+
+-- x⁻¹>x⇒x<ε : ∀ {x} → x ⁻¹ > x → x < ε
+-- x⁻¹>x⇒x<ε x⁻¹>x = ≰⇒> (<⇒≱ x⁻¹>x ∘ λ x≥ε → ≤-trans (x≥ε⇒x⁻¹≤ε x≥ε) x≥ε)
+
+-- -- _≤_
+
+---- Miscellaneous
+
+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 ⟩
   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 ⟩
+  y              ∎
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda
new file mode 100644
index 0000000..91d4b3e
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda
@@ -0,0 +1,89 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered magmas
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Magma
+  {ℓ₁ ℓ₂ ℓ₃}
+  (magma : Magma ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Magma magma
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Algebra.Definitions
+open import Data.Product using (_,_)
+open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
+
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
+
+--------------------------------------------------------------------------------
+-- Properties of _∙_
+
+---- Congruences
+
+-- _<_
+
+∙-mono-< : Congruent₂ _<_ _∙_
+∙-mono-< = invariant⇒mono-< ∙-invariant
+
+∙-monoˡ-< : LeftCongruent _<_ _∙_
+∙-monoˡ-< = invariantˡ⇒monoˡ-< ∙-invariantˡ
+
+∙-monoʳ-< : RightCongruent _<_ _∙_
+∙-monoʳ-< = invariantʳ⇒monoʳ-< ∙-invariantʳ
+
+-- _≤_
+
+∙-mono-≤ : Congruent₂ _≤_ _∙_
+∙-mono-≤ = cong+invariant⇒mono-≤ ∙-cong ∙-invariant
+
+∙-monoˡ-≤ : LeftCongruent _≤_ _∙_
+∙-monoˡ-≤ {x} = congˡ+monoˡ-<⇒monoˡ-≤ (∙-congˡ {x}) (∙-monoˡ-< {x}) {x}
+
+∙-monoʳ-≤ : RightCongruent _≤_ _∙_
+∙-monoʳ-≤ {x} = congʳ+monoʳ-<⇒monoʳ-≤ (∙-congʳ {x}) (∙-monoʳ-< {x}) {x}
+
+---- Cancelling
+
+-- _≈_
+
+∙-cancelˡ : LeftCancellative _≈_ _∙_
+∙-cancelˡ = monoˡ-<⇒cancelˡ ∙-monoˡ-<
+
+∙-cancelʳ : RightCancellative _≈_ _∙_
+∙-cancelʳ {x} = monoʳ-<⇒cancelʳ (∙-monoʳ-< {x}) {x}
+
+∙-cancel : Cancellative _≈_ _∙_
+∙-cancel = ∙-cancelˡ , ∙-cancelʳ
+
+-- _<_
+
+∙-cancelˡ-< : LeftCancellative _<_ _∙_
+∙-cancelˡ-< = monoˡ-≤⇒cancelˡ-< ∙-monoˡ-≤
+
+∙-cancelʳ-< : RightCancellative _<_ _∙_
+∙-cancelʳ-< {x} = monoʳ-≤⇒cancelʳ-< (∙-monoʳ-≤ {x}) {x}
+
+∙-cancel-< : Cancellative _<_ _∙_
+∙-cancel-< = ∙-cancelˡ-< , ∙-cancelʳ-<
+
+-- _≤_
+
+∙-cancelˡ-≤ : LeftCancellative _≤_ _∙_
+∙-cancelˡ-≤ = monoˡ-<⇒cancelˡ-≤ ∙-monoˡ-<
+
+∙-cancelʳ-≤ : RightCancellative _≤_ _∙_
+∙-cancelʳ-≤ {x} = monoʳ-<⇒cancelʳ-≤ (∙-monoʳ-< {x}) {x}
+
+∙-cancel-≤ : Cancellative _≤_ _∙_
+∙-cancel-≤ = ∙-cancelˡ-≤ , ∙-cancelʳ-≤
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda
new file mode 100644
index 0000000..220175c
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda
@@ -0,0 +1,329 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered monoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Monoid
+  {ℓ₁ ℓ₂ ℓ₃}
+  (monoid : Monoid ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Monoid monoid
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Algebra.Definitions
+open import Data.Nat as ℕ using (suc; NonZero)
+import Data.Nat.Properties as ℕₚ
+open import Function using (_∘_; flip)
+open import Function.Definitions
+open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
+open import Relation.Binary.Core
+
+open import Algebra.Properties.Monoid.Mult.TCOptimised Unordered.monoid public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup semigroup public
+  using
+  ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
+  ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
+  ; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel
+  ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
+  ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
+  )
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
+
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+
+--------------------------------------------------------------------------------
+---- Properties of _∙_
+
+---- Preserves signs
+
+-- _<_
+
+x≥ε∧y>ε⇒x∙y>ε : ∀ {x y} → x ≥ ε → y > ε → x ∙ y > ε
+x≥ε∧y>ε⇒x∙y>ε {x} {y} x≥ε y>ε = begin-strict
+  ε     ≈˘⟨ identity² ⟩
+  ε ∙ ε <⟨  ∙-monoˡ-< y>ε ⟩
+  ε ∙ y ≤⟨  ∙-monoʳ-≤ x≥ε ⟩
+  x ∙ y ∎
+
+x>ε∧y≥ε⇒x∙y>ε : ∀ {x y} → x > ε → y ≥ ε → x ∙ y > ε
+x>ε∧y≥ε⇒x∙y>ε {x} {y} x>ε y≤ε = begin-strict
+  ε     ≈˘⟨ identity² ⟩
+  ε ∙ ε ≤⟨  ∙-monoˡ-≤ y≤ε ⟩
+  ε ∙ y <⟨  ∙-monoʳ-< x>ε ⟩
+  x ∙ y ∎
+
+x≤ε∧y<ε⇒x∙y<ε : ∀ {x y} → x ≤ ε → y < ε → x ∙ y < ε
+x≤ε∧y<ε⇒x∙y<ε {x} {y} x≤ε y<ε = begin-strict
+  x ∙ y ≤⟨ ∙-monoʳ-≤ x≤ε ⟩
+  ε ∙ y <⟨ ∙-monoˡ-< y<ε ⟩
+  ε ∙ ε ≈⟨ identity² ⟩
+  ε     ∎
+
+x<ε∧y≤ε⇒x∙y<ε : ∀ {x y} → x < ε → y ≤ ε → x ∙ y < ε
+x<ε∧y≤ε⇒x∙y<ε {x} {y} x<ε y≤ε = begin-strict
+  x ∙ y <⟨ ∙-monoʳ-< x<ε ⟩
+  ε ∙ y ≤⟨ ∙-monoˡ-≤ y≤ε ⟩
+  ε ∙ ε ≈⟨ identity² ⟩
+  ε     ∎
+
+-- _≤_
+
+x≥ε∧y≥ε⇒x∙y≥ε : ∀ {x y} → x ≥ ε → y ≥ ε → x ∙ y ≥ ε
+x≥ε∧y≥ε⇒x∙y≥ε {x} {y} x≥ε y≥ε = begin
+  ε     ≈˘⟨ identity² ⟩
+  ε ∙ ε ≤⟨  ∙-mono-≤ x≥ε y≥ε ⟩
+  x ∙ y ∎
+
+x≤ε∧y≤ε⇒x∙y≤ε : ∀ {x y} → x ≤ ε → y ≤ ε → x ∙ y ≤ ε
+x≤ε∧y≤ε⇒x∙y≤ε {x} {y} x≥ε y≥ε = begin
+  x ∙ y ≤⟨ ∙-mono-≤ x≥ε y≥ε ⟩
+  ε ∙ ε ≈⟨ identity² ⟩
+  ε     ∎
+
+---- Respects signs
+
+-- _<_
+
+x≤ε∧x∙y>ε⇒y>ε : ∀ {x y} → x ≤ ε → x ∙ y > ε → y > ε
+x≤ε∧x∙y>ε⇒y>ε x≤ε x∙y>ε = ≰⇒> (<⇒≱ x∙y>ε ∘ x≤ε∧y≤ε⇒x∙y≤ε x≤ε)
+
+x≤ε∧y∙x>ε⇒y>ε : ∀ {x y} → x ≤ ε → y ∙ x > ε → y > ε
+x≤ε∧y∙x>ε⇒y>ε x≤ε y∙x>ε = ≰⇒> (<⇒≱ y∙x>ε ∘ flip x≤ε∧y≤ε⇒x∙y≤ε x≤ε)
+
+x<ε∧x∙y≥ε⇒y>ε : ∀ {x y} → x < ε → x ∙ y ≥ ε → y > ε
+x<ε∧x∙y≥ε⇒y>ε x<ε x∙y≥ε = ≰⇒> (≤⇒≯ x∙y≥ε ∘ x<ε∧y≤ε⇒x∙y<ε x<ε)
+
+x<ε∧y∙x≥ε⇒y>ε : ∀ {x y} → x < ε → y ∙ x ≥ ε → y > ε
+x<ε∧y∙x≥ε⇒y>ε x<ε y∙x≥ε = ≰⇒> (≤⇒≯ y∙x≥ε ∘ flip x≤ε∧y<ε⇒x∙y<ε x<ε)
+
+x≥ε∧x∙y<ε⇒y<ε : ∀ {x y} → x ≥ ε → x ∙ y < ε → y < ε
+x≥ε∧x∙y<ε⇒y<ε x≥ε x∙y<ε = ≰⇒> (<⇒≱ x∙y<ε ∘ x≥ε∧y≥ε⇒x∙y≥ε x≥ε)
+
+x≥ε∧y∙x<ε⇒y<ε : ∀ {x y} → x ≥ ε → y ∙ x < ε → y < ε
+x≥ε∧y∙x<ε⇒y<ε x≥ε y∙x<ε = ≰⇒> (<⇒≱ y∙x<ε ∘ flip x≥ε∧y≥ε⇒x∙y≥ε x≥ε)
+
+x>ε∧x∙y≤ε⇒y<ε : ∀ {x y} → x > ε → x ∙ y ≤ ε → y < ε
+x>ε∧x∙y≤ε⇒y<ε x>ε x∙y≤ε = ≰⇒> (≤⇒≯ x∙y≤ε ∘ x>ε∧y≥ε⇒x∙y>ε x>ε)
+
+x>ε∧y∙x≤ε⇒y<ε : ∀ {x y} → x > ε → y ∙ x ≤ ε → y < ε
+x>ε∧y∙x≤ε⇒y<ε x>ε y∙x≤ε = ≰⇒> (≤⇒≯ y∙x≤ε ∘ flip x≥ε∧y>ε⇒x∙y>ε x>ε)
+
+-- _≤_
+
+x≤ε∧x∙y≥ε⇒y≥ε : ∀ {x y} → x ≤ ε → x ∙ y ≥ ε → y ≥ ε
+x≤ε∧x∙y≥ε⇒y≥ε x≤ε x∙y≥ε = ≮⇒≥ (≤⇒≯ x∙y≥ε ∘ x≤ε∧y<ε⇒x∙y<ε x≤ε)
+
+x≤ε∧y∙x≥ε⇒y≥ε : ∀ {x y} → x ≤ ε → y ∙ x ≥ ε → y ≥ ε
+x≤ε∧y∙x≥ε⇒y≥ε x≤ε y∙x≥ε = ≮⇒≥ (≤⇒≯ y∙x≥ε ∘ flip x<ε∧y≤ε⇒x∙y<ε x≤ε)
+
+x≥ε∧x∙y≤ε⇒y≤ε : ∀ {x y} → x ≥ ε → x ∙ y ≤ ε → y ≤ ε
+x≥ε∧x∙y≤ε⇒y≤ε x≥ε x∙y≤ε = ≮⇒≥ (≤⇒≯ x∙y≤ε ∘ x≥ε∧y>ε⇒x∙y>ε x≥ε)
+
+x≥ε∧y∙x≤ε⇒y≤ε : ∀ {x y} → x ≥ ε → y ∙ x ≤ ε → y ≤ ε
+x≥ε∧y∙x≤ε⇒y≤ε x≥ε y∙x≤ε = ≮⇒≥ (≤⇒≯ y∙x≤ε ∘ flip x>ε∧y≥ε⇒x∙y>ε x≥ε)
+
+-- ---- Infer signs
+
+-- -- _≈_
+
+-- x∙y≈x⇒y≈ε : ∀ {x y} → x ∙ y ≈ x → y ≈ ε
+-- x∙y≈x⇒y≈ε {x} {y} x∙y≈x = ∙-cancelˡ x (Eq.trans x∙y≈x (Eq.sym (identityʳ x)))
+
+-- x∙y≈y⇒x≈ε : ∀ {x y} → x ∙ y ≈ y → x ≈ ε
+-- x∙y≈y⇒x≈ε {x} {y} x∙y≈y = ∙-cancelʳ x ε (Eq.trans x∙y≈y (Eq.sym (identityˡ y)))
+
+-- -- _<_
+
+-- x∙y<x⇒y<ε : ∀ {x y} → x ∙ y < x → y < ε
+-- x∙y<x⇒y<ε {x} {y} x∙y<x = ∙-cancelˡ-< x (<-respʳ-≈ (Eq.sym (identityʳ x)) x∙y<x)
+
+-- x∙y<y⇒x<ε : ∀ {x y} → x ∙ y < y → x < ε
+-- x∙y<y⇒x<ε {x} {y} x∙y<y = ∙-cancelʳ-< x ε (<-respʳ-≈ (Eq.sym (identityˡ y)) x∙y<y)
+
+-- x∙y>x⇒y>ε : ∀ {x y} → x ∙ y > x → y > ε
+-- x∙y>x⇒y>ε {x} {y} x∙y>x = ∙-cancelˡ-< x (<-respˡ-≈ (Eq.sym (identityʳ x)) x∙y>x)
+
+-- x∙y>y⇒x>ε : ∀ {x y} → x ∙ y > y → x > ε
+-- x∙y>y⇒x>ε {x} {y} x∙y>y = ∙-cancelʳ-< ε x (<-respˡ-≈ (Eq.sym (identityˡ y)) x∙y>y)
+
+-- -- _≤_
+
+-- x∙y≤x⇒y≤ε : ∀ {x y} → x ∙ y ≤ x → y ≤ ε
+-- x∙y≤x⇒y≤ε {x} {y} x∙y≤x = ∙-cancelˡ-≤ x (≤-respʳ-≈ (Eq.sym (identityʳ x)) x∙y≤x)
+
+-- x∙y≤y⇒x≤ε : ∀ {x y} → x ∙ y ≤ y → x ≤ ε
+-- x∙y≤y⇒x≤ε {x} {y} x∙y≤y = ∙-cancelʳ-≤ x ε (≤-respʳ-≈ (Eq.sym (identityˡ y)) x∙y≤y)
+
+-- x∙y≥x⇒y≥ε : ∀ {x y} → x ∙ y ≥ x → y ≥ ε
+-- x∙y≥x⇒y≥ε {x} {y} x∙y≥x = ∙-cancelˡ-≤ x (≤-respˡ-≈ (Eq.sym (identityʳ x)) x∙y≥x)
+
+-- x∙y≥y⇒x≥ε : ∀ {x y} → x ∙ y ≥ y → x ≥ ε
+-- x∙y≥y⇒x≥ε {x} {y} x∙y≥y = ∙-cancelʳ-≤ ε x (≤-respˡ-≈ (Eq.sym (identityˡ y)) x∙y≥y)
+
+-- --------------------------------------------------------------------------------
+---- Properties of _×_
+
+---- Zero
+
+×-zeroˡ : ∀ x → 0 × x ≈ ε
+×-zeroˡ x = Eq.refl
+
+×-zeroʳ : ∀ n → n × ε ≈ ε
+×-zeroʳ 0       = Eq.refl
+×-zeroʳ (suc n) = begin-equality
+  suc n × ε ≈⟨ 1+× n ε ⟩
+  ε ∙ n × ε ≈⟨ ∙-congˡ (×-zeroʳ n) ⟩
+  ε ∙ ε     ≈⟨ identity² ⟩
+  ε         ∎
+
+---- Identity
+
+×-identityˡ : ∀ x → 1 × x ≈ x
+×-identityˡ x = Eq.refl
+
+---- Preserves signs
+
+-- _≤_
+
+x≥ε⇒n×x≥ε : ∀ n {x} → x ≥ ε → n × x ≥ ε
+x≥ε⇒n×x≥ε 0       {x} x≥ε = ≤-refl
+x≥ε⇒n×x≥ε (suc n) {x} x≥ε = begin
+  ε         ≤⟨  x≥ε∧y≥ε⇒x∙y≥ε x≥ε (x≥ε⇒n×x≥ε n x≥ε) ⟩
+  x ∙ n × x ≈˘⟨ 1+× n x ⟩
+  suc n × x ∎
+
+x≤ε⇒n×x≤ε : ∀ n {x} → x ≤ ε → n × x ≤ ε
+x≤ε⇒n×x≤ε 0       {x} x≤ε = ≤-refl
+x≤ε⇒n×x≤ε (suc n) {x} x≤ε = begin
+  suc n × x ≈⟨ 1+× n x ⟩
+  x ∙ n × x ≤⟨ x≤ε∧y≤ε⇒x∙y≤ε x≤ε (x≤ε⇒n×x≤ε n x≤ε) ⟩
+  ε         ∎
+
+-- _<_
+
+n≢0∧x>ε⇒n×x>ε : ∀ n {x} → ⦃ NonZero n ⦄ → x > ε → n × x > ε
+n≢0∧x>ε⇒n×x>ε (suc n) {x} x>ε = begin-strict
+  ε         <⟨  x>ε∧y≥ε⇒x∙y>ε x>ε (x≥ε⇒n×x≥ε n (<⇒≤ x>ε)) ⟩
+  x ∙ n × x ≈˘⟨ 1+× n x ⟩
+  suc n × x ∎
+
+n≢0∧x<ε⇒n×x<ε : ∀ n {x} → ⦃ NonZero n ⦄ → x < ε → n × x < ε
+n≢0∧x<ε⇒n×x<ε (suc n) {x} x<ε = begin-strict
+  suc n × x ≈⟨ 1+× n x ⟩
+  x ∙ n × x <⟨ x<ε∧y≤ε⇒x∙y<ε x<ε (x≤ε⇒n×x≤ε n (<⇒≤ x<ε)) ⟩
+  ε         ∎
+
+---- Congruences
+
+-- _≤_
+
+×-monoˡ-≤ : ∀ n → Congruent₁ _≤_ (n ×_)
+×-monoˡ-≤ 0               x≤y = ≤-refl
+×-monoˡ-≤ (suc n) {x} {y} x≤y = begin
+  suc n × x ≈⟨  1+× n x ⟩
+  x ∙ n × x ≤⟨  ∙-mono-≤ x≤y (×-monoˡ-≤ n x≤y) ⟩
+  y ∙ n × y ≈˘⟨ 1+× n y ⟩
+  suc n × y ∎
+
+x≥ε⇒×-monoʳ-≤ : ∀ {x} → x ≥ ε → (_× x) Preserves ℕ._≤_ ⟶ _≤_
+x≥ε⇒×-monoʳ-≤ {x} x≥ε {.0}     {n}      ℕ.z≤n       = x≥ε⇒n×x≥ε n x≥ε
+x≥ε⇒×-monoʳ-≤ {x} x≥ε {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin
+  suc m × x ≈⟨  1+× m x ⟩
+  x ∙ m × x ≤⟨  ∙-monoˡ-≤ (x≥ε⇒×-monoʳ-≤ x≥ε m≤n) ⟩
+  x ∙ n × x ≈˘⟨ 1+× n x ⟩
+  suc n × x ∎
+
+x≤ε⇒×-anti-monoʳ-≤ : ∀ {x} → x ≤ ε → (_× x) Preserves ℕ._≤_ ⟶ _≥_
+x≤ε⇒×-anti-monoʳ-≤ {x} x≤ε {.0}     {n}      ℕ.z≤n       = x≤ε⇒n×x≤ε n x≤ε
+x≤ε⇒×-anti-monoʳ-≤ {x} x≤ε {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin
+  suc n × x ≈⟨  1+× n x ⟩
+  x ∙ n × x ≤⟨  ∙-monoˡ-≤ (x≤ε⇒×-anti-monoʳ-≤ x≤ε m≤n) ⟩
+  x ∙ m × x ≈˘⟨ 1+× m x ⟩
+  suc m × x ∎
+
+-- _<_
+
+n≢0⇒×-monoˡ-< : ∀ n → ⦃ NonZero n ⦄ → Congruent₁ _<_ (n ×_)
+n≢0⇒×-monoˡ-< (suc n) {x} {y} x<y = begin-strict
+  suc n × x ≈⟨  1+× n x ⟩
+  x ∙ n × x ≤⟨  ∙-monoˡ-≤ (×-monoˡ-≤ n (<⇒≤ x<y)) ⟩
+  x ∙ n × y <⟨  ∙-monoʳ-< x<y ⟩
+  y ∙ n × y ≈˘⟨ 1+× n y ⟩
+  suc n × y ∎
+
+x>ε⇒×-monoʳ-< : ∀ {x} → x > ε → (_× x) Preserves ℕ._<_ ⟶ _<_
+x>ε⇒×-monoʳ-< {x} x>ε {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict
+  m × x     ≈˘⟨ identityˡ (m × x) ⟩
+  ε ∙ m × x ≤⟨  ∙-monoˡ-≤ (x≥ε⇒×-monoʳ-≤ (<⇒≤ x>ε) m≤n) ⟩
+  ε ∙ n × x <⟨  ∙-monoʳ-< x>ε ⟩
+  x ∙ n × x ≈˘⟨ 1+× n x ⟩
+  suc n × x ∎
+
+x<ε⇒×-anti-monoʳ-< : ∀ {x} → x < ε → (_× x) Preserves ℕ._<_ ⟶ _>_
+x<ε⇒×-anti-monoʳ-< {x} x<ε {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict
+  suc n × x ≈⟨ 1+× n x ⟩
+  x ∙ n × x <⟨ ∙-monoʳ-< x<ε ⟩
+  ε ∙ n × x ≤⟨ ∙-monoˡ-≤ (x≤ε⇒×-anti-monoʳ-≤ (<⇒≤ x<ε) m≤n) ⟩
+  ε ∙ m × x ≈⟨ identityˡ (m × x) ⟩
+  m × x     ∎
+
+---- Cancellative
+
+-- _<_
+
+×-cancelˡ-< : ∀ n → Injective _<_ _<_ (n ×_)
+×-cancelˡ-< n = mono₁-≤⇒cancel₁-< (×-monoˡ-≤ n)
+
+x≥ε⇒×-cancelʳ-< : ∀ {x} → x ≥ ε → Injective ℕ._<_ _<_ (_× x)
+x≥ε⇒×-cancelʳ-< x≥ε m×x<n×x = ℕₚ.≰⇒> (<⇒≱ m×x<n×x ∘ x≥ε⇒×-monoʳ-≤ x≥ε)
+
+x≤ε⇒×-anti-cancelʳ-< : ∀ {x} → x ≤ ε → Injective ℕ._<_ _>_ (_× x)
+x≤ε⇒×-anti-cancelʳ-< x≤ε m×x>n×x = ℕₚ.≰⇒> (<⇒≱ m×x>n×x ∘ x≤ε⇒×-anti-monoʳ-≤ x≤ε)
+
+-- _≤_
+
+n≢0⇒×-cancelˡ-≤ : ∀ n → ⦃ NonZero n ⦄ → Injective _≤_ _≤_ (n ×_)
+n≢0⇒×-cancelˡ-≤ n = mono₁-<⇒cancel₁-≤ (n≢0⇒×-monoˡ-< n)
+
+x>ε⇒×-cancelʳ-≤ : ∀ {x} → x > ε → Injective ℕ._≤_ _≤_ (_× x)
+x>ε⇒×-cancelʳ-≤ x>ε m×x≤n×x = ℕₚ.≮⇒≥ (≤⇒≯ m×x≤n×x ∘ x>ε⇒×-monoʳ-< x>ε)
+
+x<ε⇒×-anti-cancelʳ-≤ : ∀ {x} → x < ε → Injective ℕ._≤_ _≥_ (_× x)
+x<ε⇒×-anti-cancelʳ-≤ x<ε m×x≥n×x = ℕₚ.≮⇒≥ (≤⇒≯ m×x≥n×x ∘ x<ε⇒×-anti-monoʳ-< x<ε)
+
+---- Respects signs
+
+-- _<_
+
+n×x>ε⇒x>ε : ∀ {n x} → n × x > ε → x > ε
+n×x>ε⇒x>ε {n} n×x>ε = ≰⇒> (<⇒≱ n×x>ε ∘ x≤ε⇒n×x≤ε n)
+
+n×x<ε⇒x<ε : ∀ {n x} → n × x < ε → x < ε
+n×x<ε⇒x<ε {n} n×x<ε = ≰⇒> (<⇒≱ n×x<ε ∘ x≥ε⇒n×x≥ε n)
+
+-- _≥_
+
+n≢0∧n×x≥ε⇒x≥ε : ∀ {n x} → ⦃ NonZero n ⦄ → n × x ≥ ε → x ≥ ε
+n≢0∧n×x≥ε⇒x≥ε {n} n×x≥ε = ≮⇒≥ (≤⇒≯ n×x≥ε ∘ n≢0∧x<ε⇒n×x<ε n)
+
+n≢0∧n×x≤ε⇒x≤ε : ∀ {n x} → ⦃ NonZero n ⦄ → n × x ≤ ε → x ≤ ε
+n≢0∧n×x≤ε⇒x≤ε {n} n×x≤ε = ≮⇒≥ (≤⇒≯ n×x≤ε ∘ n≢0∧x>ε⇒n×x>ε n)
+
+-- ---- Infer signs
+
+-- -- _≈_
+
+-- n≢0∧n×x≈x⇒x≈ε : ∀ n {x} → ⦃ NonZero n ⦄ → n × x ≈ x → x ≈ ε
+-- n≢0∧n×x≈x⇒x≈ε n n×x≈x = ≮∧≯⇒≈
+--   (λ x<ε → <-irrefl n×x≈x (<-trans (n≢0∧x<ε⇒n×x<ε {!!} {!!}) {!!}))
+--   (λ x>ε → {!!})
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
index 484143c..5e51e89 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -14,68 +14,542 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.Ring
   where
 
 open Ring ring
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
+  )
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.FromNeg
-open import Data.Nat using (suc; NonZero)
+open import Algebra.Definitions
+open import Data.Nat as ℕ using (suc; NonZero)
 open import Data.Sum using (inj₁; inj₂)
-open import Data.Unit.Polymorphic using (⊤)
-open import Relation.Binary using (tri<; tri≈; tri>)
+open import Function using (_∘_)
+open import Function.Definitions
+open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
 open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
 
 open import Algebra.Properties.Ring Unordered.ring public
   renaming (-0#≈0# to -0≈0)
+
 open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
 open import Algebra.Properties.Semiring.Exp.TCOptimised Unordered.semiring public
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
 open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelianGroup public
-  using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>)
+  using
+  ( ×-zeroˡ; ×-zeroʳ
+  ; ×-identityˡ
+  ; n≢0⇒×-monoˡ-<; ×-monoˡ-≤
+  ; ×-cancelˡ-<; n≢0⇒×-cancelˡ-≤
+  )
   renaming
-    ( x<y⇒ε<yx⁻¹ to x<y⇒0<y-x
-    ; ⁻¹-anti-mono to -‿anti-mono
-    )
-
-instance
-  ⊤′ : ∀ {ℓ} → ⊤ {ℓ = ℓ}
-  ⊤′ = _
-
-  number : Number Carrier
-  number = record
-    { Constraint = λ _ → ⊤
-    ; fromNat = _× 1#
-    }
-
-  negative : Negative Carrier
-  negative = record
-    { Constraint = λ _ → ⊤
-    ; fromNeg = λ x → - (x × 1#)
-    }
-
-0≤1 : 0 ≤ 1
-0≤1 with compare 0 1
-... | tri< 0<1 _ _ = inj₁ 0<1
-... | tri≈ _ 0≈1 _ = inj₂ 0≈1
-... | tri> _ _ 0>1 = inj₁ (begin-strict
-  0          <⟨  0<a+0<b⇒0<ab 0<-1 0<-1 ⟩
-  -1 * -1    ≈˘⟨ -‿distribˡ-* 1 -1 ⟩
-  - (1 * -1) ≈⟨  -‿cong (*-identityˡ -1) ⟩
-  - -1       ≈⟨  -‿involutive 1 ⟩
-  1          ∎)
-  where
-  0<-1 = begin-strict
-    0   ≈˘⟨ -0≈0 ⟩
-    - 0 <⟨  -‿anti-mono 0>1 ⟩
-    -1  ∎
-
-1≉0+n≉0⇒0<+n : 1 ≉ 0 → ∀ n → {{NonZero n}} → 0 < fromNat n
-1≉0+n≉0⇒0<+n 1≉0 (suc 0)       = ≥∧≉⇒> 0≤1 1≉0
-1≉0+n≉0⇒0<+n 1≉0 (suc (suc n)) = begin-strict
-  0                   ≈˘⟨ +-identity² ⟩
-  0 + 0               <⟨  +-invariantˡ 0 (≥∧≉⇒> 0≤1 1≉0) ⟩
-  0 + 1               <⟨  +-invariantʳ 1 (1≉0+n≉0⇒0<+n 1≉0 (suc n)) ⟩
-  fromNat (suc n) + 1 ∎
-
-1≉0+n≉0⇒-n<0 : 1 ≉ 0 → ∀ n → {{NonZero n}} → fromNeg n < 0
-1≉0+n≉0⇒-n<0 1≉0 n = begin-strict
-  - fromNat n <⟨ -‿anti-mono (1≉0+n≉0⇒0<+n 1≉0 n) ⟩
-  - 0         ≈⟨ -0≈0 ⟩
-  0           ∎
+  ( ∙-mono-<  to +-mono-<
+  ; ∙-monoˡ-< to +-monoˡ-<
+  ; ∙-monoʳ-< to +-monoʳ-<
+  ; ∙-mono-≤  to +-mono-≤
+  ; ∙-monoˡ-≤ to +-monoˡ-≤
+  ; ∙-monoʳ-≤ to +-monoʳ-≤
+
+  ; ∙-cancelˡ-< to +-cancelˡ-<
+  ; ∙-cancelʳ-< to +-cancelʳ-<
+  ; ∙-cancel-<  to +-cancel-<
+  ; ∙-cancelˡ-≤ to +-cancelˡ-≤
+  ; ∙-cancelʳ-≤ to +-cancelʳ-≤
+  ; ∙-cancel-≤  to +-cancel-≤
+  -- _∙_ pres signs
+  ; x≥ε∧y>ε⇒x∙y>ε to x≥0∧y>0⇒x+y>0
+  ; x>ε∧y≥ε⇒x∙y>ε to x>0∧y≥0⇒x+y>0
+  ; x≤ε∧y<ε⇒x∙y<ε to x≤0∧y<0⇒x+y<0
+  ; x<ε∧y≤ε⇒x∙y<ε to x<0∧y≤0⇒x+y<0
+  ; x≥ε∧y≥ε⇒x∙y≥ε to x≥0∧y≥0⇒x+y≥0
+  ; x≤ε∧y≤ε⇒x∙y≤ε to x≤0∧y≤0⇒x+y≤0
+  -- _∙_ resp signs
+  ; x≤ε∧x∙y>ε⇒y>ε to x≤0∧x+y>0⇒y>0
+  ; x≤ε∧y∙x>ε⇒y>ε to x≤0∧y+x>0⇒y>0
+  ; x<ε∧x∙y≥ε⇒y>ε to x<0∧x+y≥0⇒y>0
+  ; x<ε∧y∙x≥ε⇒y>ε to x<0∧y+x≥0⇒y>0
+  ; x≥ε∧x∙y<ε⇒y<ε to x≥0∧x+y<0⇒y<0
+  ; x≥ε∧y∙x<ε⇒y<ε to x≥0∧y+x<0⇒y<0
+  ; x>ε∧x∙y≤ε⇒y<ε to x>0∧x+y≤0⇒y<0
+  ; x>ε∧y∙x≤ε⇒y<ε to x>0∧y+x≤0⇒y<0
+  ; x≤ε∧x∙y≥ε⇒y≥ε to x≤0∧x+y≥0⇒y≥0
+  ; x≤ε∧y∙x≥ε⇒y≥ε to x≤0∧y+x≥0⇒y≥0
+  ; x≥ε∧x∙y≤ε⇒y≤ε to x≥0∧x+y≤0⇒y≤0
+  ; x≥ε∧y∙x≤ε⇒y≤ε to x≥0∧y+x≤0⇒y≤0
+
+  ; x>ε⇒×-monoʳ-<      to x>0⇒×-monoʳ-<
+  ; x<ε⇒×-anti-monoʳ-< to x<0⇒×-anti-monoʳ-<
+  ; x≥ε⇒×-monoʳ-≤      to x≥0⇒×-monoʳ-≤
+  ; x≤ε⇒×-anti-monoʳ-≤ to x≤0⇒×-anti-monoʳ-≤
+
+  ; x≥ε⇒×-cancelʳ-<      to x≥0⇒×-cancelʳ-<
+  ; x≤ε⇒×-anti-cancelʳ-< to x≤0⇒×-anti-cancelʳ-<
+  ; x>ε⇒×-cancelʳ-≤      to x>0⇒×-cancelʳ-≤
+  ; x<ε⇒×-anti-cancelʳ-≤ to x<0⇒×-anti-cancelʳ-≤
+  -- _×_ pres signs
+  ; n≢0∧x>ε⇒n×x>ε to n≢0∧x>0⇒n×x>0
+  ; n≢0∧x<ε⇒n×x<ε to n≢0∧x<0⇒n×x<0
+  ; x≥ε⇒n×x≥ε     to x≥0⇒n×x≥0
+  ; x≤ε⇒n×x≤ε     to x≤0⇒n×x≤0
+  -- _×_ resp signs
+  ; n×x>ε⇒x>ε     to n×x>0⇒x>0
+  ; n×x<ε⇒x<ε     to n×x<0⇒x<0
+  ; n≢0∧n×x≥ε⇒x≥ε to n≢0∧n×x≥0⇒x≥0
+  ; n≢0∧n×x≤ε⇒x≤ε to n≢0∧n×x≤0⇒x≤0
+
+  ; ⁻¹-anti-mono-< to -‿anti-mono-<
+  ; ⁻¹-anti-mono-≤ to -‿anti-mono-≤
+
+  ; ⁻¹-cancel        to -‿cancel
+  ; ⁻¹-anti-cancel-< to -‿anti-cancel-<
+  ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤
+
+  ; x<ε⇒x⁻¹>ε to x<0⇒-x>0
+  ; x>ε⇒x⁻¹<ε to x>0⇒-x<0
+  ; x≤ε⇒x⁻¹≥ε to x≤0⇒-x≥0
+  ; x≥ε⇒x⁻¹≤ε to x≥0⇒-x≤0
+
+  ; x⁻¹<ε⇒x>ε to -x<0⇒x>0
+  ; x⁻¹>ε⇒x<ε to -x>0⇒x<0
+  ; x⁻¹≤ε⇒x≥ε to -x≤0⇒x≥0
+  ; x⁻¹≥ε⇒x≤ε to -x≥0⇒x≤0
+
+  ; x<y⇒ε<y∙x⁻¹ to x<y⇒0<y-x
+  ; ε<y∙x⁻¹⇒x<y to 0<y-x⇒x<y
+  )
+
+--------------------------------------------------------------------------------
+---- Properties of _*_ and -_
+
+-x*-y≈x*y : ∀ x y → - x * - y ≈ x * y
+-x*-y≈x*y x y = begin-equality
+  - x * - y   ≈˘⟨ -‿distribˡ-* x (- y) ⟩
+  - (x * - y) ≈˘⟨ -‿cong (-‿distribʳ-* x y) ⟩
+  - - (x * y) ≈⟨  -‿involutive (x * y) ⟩
+  x * y       ∎
+
+--------------------------------------------------------------------------------
+---- Properties of _*_
+
+---- Congruences
+
+-- _<_
+
+x>0⇒*-monoˡ-< : ∀ {x} → x > 0# → Congruent₁ _<_ (x *_)
+x>0⇒*-monoˡ-< {x} x>0 {y} {z} y<z = begin-strict
+  x * y                         ≈˘⟨ +-identityˡ (x * y) ⟩
+  0# + x * y                    ≈˘⟨ +-cong (-‿inverseʳ (x * z)) (-x*-y≈x*y x y) ⟩
+  x * z - x * z + - x * - y     ≈⟨  +-congʳ (+-congˡ (-‿distribˡ-* x z)) ⟩
+  x * z + - x * z + - x * - y   ≈⟨  +-assoc (x * z) (- x * z) (- x * - y) ⟩
+  x * z + (- x * z + - x * - y) ≈˘⟨ +-congˡ (distribˡ (- x) z (- y)) ⟩
+  x * z + - x * (z - y)         ≈˘⟨ +-congˡ (-‿distribˡ-* x (z - y)) ⟩
+  x * z - x * (z - y)           <⟨  +-monoˡ-< (x>0⇒-x<0 (x>0∧y>0⇒x*y>0 x>0 (x<y⇒0<y-x y<z))) ⟩
+  x * z + 0#                    ≈⟨  +-identityʳ (x * z) ⟩
+  x * z                         ∎
+
+x>0⇒*-monoʳ-< : ∀ {x} → x > 0# → Congruent₁ _<_ (_* x)
+x>0⇒*-monoʳ-< {x} x>0 {y} {z} y<z = begin-strict
+  y * x                         ≈˘⟨ +-identityˡ (y * x) ⟩
+  0# + y * x                    ≈˘⟨ +-cong (-‿inverseʳ (z * x)) (-x*-y≈x*y y x) ⟩
+  z * x - z * x + - y * - x     ≈⟨  +-congʳ (+-congˡ (-‿distribʳ-* z x)) ⟩
+  z * x + z * - x + - y * - x   ≈⟨  +-assoc (z * x) (z * - x) (- y * - x) ⟩
+  z * x + (z * - x + - y * - x) ≈˘⟨ +-congˡ (distribʳ (- x) z (- y)) ⟩
+  z * x + (z - y) * - x         ≈˘⟨ +-congˡ (-‿distribʳ-* (z - y) x) ⟩
+  z * x - (z - y) * x           <⟨  +-monoˡ-< (x>0⇒-x<0 (x>0∧y>0⇒x*y>0 (x<y⇒0<y-x y<z) x>0)) ⟩
+  z * x + 0#                    ≈⟨  +-identityʳ (z * x) ⟩
+  z * x                         ∎
+
+x<0⇒*-anti-monoˡ-< : ∀ {x} → x < 0# → (x *_) Preserves _<_ ⟶ _>_
+x<0⇒*-anti-monoˡ-< {x} x<0 {y} {z} y<z = begin-strict
+  x * z                         ≈˘⟨ +-identityʳ (x * z) ⟩
+  x * z + 0#                    <⟨  +-monoˡ-< (x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) (x<y⇒0<y-x y<z)) ⟩
+  x * z + - x * (z - y)         ≈⟨  +-congˡ (distribˡ (- x) z (- y)) ⟩
+  x * z + (- x * z + - x * - y) ≈˘⟨ +-assoc (x * z) (- x * z) (- x * - y) ⟩
+  x * z + - x * z + - x * - y   ≈˘⟨ +-congʳ (+-congˡ (-‿distribˡ-* x z)) ⟩
+  x * z - x * z + - x * - y     ≈⟨  +-cong (-‿inverseʳ (x * z)) (-x*-y≈x*y x y) ⟩
+  0# + x * y                    ≈⟨  +-identityˡ (x * y) ⟩
+  x * y                         ∎
+
+x<0⇒*-anti-monoʳ-< : ∀ {x} → x < 0# → (_* x) Preserves _<_ ⟶ _>_
+x<0⇒*-anti-monoʳ-< {x} x<0 {y} {z} y<z = begin-strict
+  z * x                         ≈˘⟨ +-identityʳ (z * x) ⟩
+  z * x + 0#                    <⟨  +-monoˡ-< (x>0∧y>0⇒x*y>0 (x<y⇒0<y-x y<z) (x<0⇒-x>0 x<0)) ⟩
+  z * x + (z - y) * - x         ≈⟨  +-congˡ (distribʳ (- x) z (- y)) ⟩
+  z * x + (z * - x + - y * - x) ≈˘⟨ +-assoc (z * x) (z * - x) (- y * - x) ⟩
+  z * x + z * - x + - y * - x   ≈˘⟨ +-congʳ (+-congˡ (-‿distribʳ-* z x)) ⟩
+  z * x - z * x + - y * - x     ≈⟨  +-cong (-‿inverseʳ (z * x)) (-x*-y≈x*y y x) ⟩
+  0# + y * x                    ≈⟨  +-identityˡ (y * x) ⟩
+  y * x                         ∎
+
+-- _≤_
+
+x≥0⇒*-monoˡ-≤ : ∀ {x} → x ≥ 0# → Congruent₁ _≤_ (x *_)
+x≥0⇒*-monoˡ-≤     (inj₁ x>0)         y≤z = cong₁+mono₁-<⇒mono₁-≤ *-congˡ (x>0⇒*-monoˡ-< x>0) y≤z
+x≥0⇒*-monoˡ-≤ {x} (inj₂ 0≈x) {y} {z} y≤z = ≤-reflexive (begin-equality
+  x * y  ≈˘⟨ *-congʳ 0≈x ⟩
+  0# * y ≈⟨  zeroˡ y ⟩
+  0#     ≈˘⟨ zeroˡ z ⟩
+  0# * z ≈⟨  *-congʳ 0≈x ⟩
+  x * z  ∎)
+
+x≥0⇒*-monoʳ-≤ : ∀ {x} → x ≥ 0# → Congruent₁ _≤_ (_* x)
+x≥0⇒*-monoʳ-≤     (inj₁ x>0)         y≤z = cong₁+mono₁-<⇒mono₁-≤ *-congʳ (x>0⇒*-monoʳ-< x>0) y≤z
+x≥0⇒*-monoʳ-≤ {x} (inj₂ 0≈x) {y} {z} y≤z = ≤-reflexive (begin-equality
+  y * x  ≈˘⟨ *-congˡ 0≈x ⟩
+  y * 0# ≈⟨  zeroʳ y ⟩
+  0#     ≈˘⟨ zeroʳ z ⟩
+  z * 0# ≈⟨  *-congˡ 0≈x ⟩
+  z * x  ∎)
+
+x≤0⇒*-anti-monoˡ-≤ : ∀ {x} → x ≤ 0# → (x *_) Preserves _≤_ ⟶ _≥_
+x≤0⇒*-anti-monoˡ-≤     (inj₁ x<0)         y≤z = cong₁+anti-mono₁-<⇒anti-mono₁-≤ *-congˡ (x<0⇒*-anti-monoˡ-< x<0) y≤z
+x≤0⇒*-anti-monoˡ-≤ {x} (inj₂ x≈0) {y} {z} y≤z = ≤-reflexive (begin-equality
+  x * z  ≈⟨  *-congʳ x≈0 ⟩
+  0# * z ≈⟨  zeroˡ z ⟩
+  0#     ≈˘⟨ zeroˡ y ⟩
+  0# * y ≈˘⟨ *-congʳ x≈0 ⟩
+  x * y  ∎)
+
+x≤0⇒*-anti-monoʳ-≤ : ∀ {x} → x ≤ 0# → (_* x) Preserves _≤_ ⟶ _≥_
+x≤0⇒*-anti-monoʳ-≤     (inj₁ x<0)         y≤z = cong₁+anti-mono₁-<⇒anti-mono₁-≤ *-congʳ (x<0⇒*-anti-monoʳ-< x<0) y≤z
+x≤0⇒*-anti-monoʳ-≤ {x} (inj₂ x≈0) {y} {z} y≤z = ≤-reflexive (begin-equality
+  z * x  ≈⟨  *-congˡ x≈0 ⟩
+  z * 0# ≈⟨  zeroʳ z ⟩
+  0#     ≈˘⟨ zeroʳ y ⟩
+  y * 0# ≈˘⟨ *-congˡ x≈0 ⟩
+  y * x  ∎)
+
+---- Cancellative
+
+-- _≈_
+
+x>0⇒*-cancelˡ : ∀ {x} → x > 0# → Injective _≈_ _≈_ (x *_)
+x>0⇒*-cancelˡ x>0 = mono₁-<⇒cancel₁ (x>0⇒*-monoˡ-< x>0)
+
+x>0⇒*-cancelʳ : ∀ {x} → x > 0# → Injective _≈_ _≈_ (_* x)
+x>0⇒*-cancelʳ x>0 = mono₁-<⇒cancel₁ (x>0⇒*-monoʳ-< x>0)
+
+x<0⇒*-cancelˡ : ∀ {x} → x < 0# → Injective _≈_ _≈_ (x *_)
+x<0⇒*-cancelˡ x<0 = anti-mono₁-<⇒cancel₁ (x<0⇒*-anti-monoˡ-< x<0)
+
+x<0⇒*-cancelʳ : ∀ {x} → x < 0# → Injective _≈_ _≈_ (_* x)
+x<0⇒*-cancelʳ x<0 = anti-mono₁-<⇒cancel₁ (x<0⇒*-anti-monoʳ-< x<0)
+
+-- _<_
+
+x≥0⇒*-cancelˡ-< : ∀ {x} → x ≥ 0# → Injective _<_ _<_ (x *_)
+x≥0⇒*-cancelˡ-< = mono₁-≤⇒cancel₁-< ∘ x≥0⇒*-monoˡ-≤
+
+x≥0⇒*-cancelʳ-< : ∀ {x} → x ≥ 0# → Injective _<_ _<_ (_* x)
+x≥0⇒*-cancelʳ-< = mono₁-≤⇒cancel₁-< ∘ x≥0⇒*-monoʳ-≤
+
+x≤0⇒*-anti-cancelˡ-< : ∀ {x} → x ≤ 0# → Injective _<_ _>_ (x *_)
+x≤0⇒*-anti-cancelˡ-< = anti-mono₁-≤⇒anti-cancel₁-< ∘ x≤0⇒*-anti-monoˡ-≤
+
+x≤0⇒*-anti-cancelʳ-< : ∀ {x} → x ≤ 0# → Injective _<_ _>_ (_* x)
+x≤0⇒*-anti-cancelʳ-< = anti-mono₁-≤⇒anti-cancel₁-< ∘ x≤0⇒*-anti-monoʳ-≤
+
+-- _≤_
+
+x>0⇒*-cancelˡ-≤ : ∀ {x} → x > 0# → Injective _≤_ _≤_ (x *_)
+x>0⇒*-cancelˡ-≤ = mono₁-<⇒cancel₁-≤ ∘ x>0⇒*-monoˡ-<
+
+x>0⇒*-cancelʳ-≤ : ∀ {x} → x > 0# → Injective _≤_ _≤_ (_* x)
+x>0⇒*-cancelʳ-≤ = mono₁-<⇒cancel₁-≤ ∘ x>0⇒*-monoʳ-<
+
+x<0⇒*-anti-cancelˡ-≤ : ∀ {x} → x < 0# → Injective _≤_ _≥_ (x *_)
+x<0⇒*-anti-cancelˡ-≤ = anti-mono₁-<⇒anti-cancel₁-≤ ∘ x<0⇒*-anti-monoˡ-<
+
+x<0⇒*-anti-cancelʳ-≤ : ∀ {x} → x < 0# → Injective _≤_ _≥_ (_* x)
+x<0⇒*-anti-cancelʳ-≤ = anti-mono₁-<⇒anti-cancel₁-≤ ∘ x<0⇒*-anti-monoʳ-<
+
+---- Preserves signs
+
+-- _≈_
+
+x≈0⇒x*y≈0 : ∀ {x} → x ≈ 0# → ∀ y → x * y ≈ 0#
+x≈0⇒x*y≈0 {x} x≈0 y = begin-equality
+  x * y  ≈⟨ *-congʳ x≈0 ⟩
+  0# * y ≈⟨ zeroˡ y ⟩
+  0#     ∎
+
+x≈0⇒y*x≈0 : ∀ {x} → x ≈ 0# → ∀ y → y * x ≈ 0#
+x≈0⇒y*x≈0 {x} x≈0 y = begin-equality
+  y * x  ≈⟨ *-congˡ x≈0 ⟩
+  y * 0# ≈⟨ zeroʳ y ⟩
+  0#     ∎
+
+-- _<_
+
+-- Have x>0∧y>0⇒x*y>0 by ring
+
+x>0∧y<0⇒x*y<0 : ∀ {x y} → x > 0# → y < 0# → x * y < 0#
+x>0∧y<0⇒x*y<0 {x} {y} x>0 y<0 = -x>0⇒x<0 (begin-strict
+  0#        <⟨  x>0∧y>0⇒x*y>0 x>0 (x<0⇒-x>0 y<0) ⟩
+  x * - y   ≈˘⟨ -‿distribʳ-* x y ⟩
+  - (x * y) ∎)
+
+x<0∧y>0⇒x*y<0 : ∀ {x y} → x < 0# → y > 0# → x * y < 0#
+x<0∧y>0⇒x*y<0 {x} {y} x<0 y>0 = -x>0⇒x<0 (begin-strict
+  0#        <⟨  x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) y>0  ⟩
+  - x * y   ≈˘⟨ -‿distribˡ-* x y ⟩
+  - (x * y) ∎)
+
+x<0∧y<0⇒x*y>0 : ∀ {x y} → x < 0# → y < 0# → x * y > 0#
+x<0∧y<0⇒x*y>0 {x} {y} x<0 y<0 = begin-strict
+  0#        <⟨ x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) (x<0⇒-x>0 y<0) ⟩
+  - x * - y ≈⟨ -x*-y≈x*y x y ⟩
+  x * y     ∎
+
+-- _≤_
+
+x≥0∧y≥0⇒x*y≥0 : ∀ {x y} → x ≥ 0# → y ≥ 0# → x * y ≥ 0#
+x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₁ x>0) (inj₁ y>0) = <⇒≤ (x>0∧y>0⇒x*y>0 x>0 y>0)
+x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₁ x>0) (inj₂ 0≈y) = ≤-reflexive (Eq.sym (x≈0⇒y*x≈0 (Eq.sym 0≈y) x))
+x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₂ 0≈x) y≥0        = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 (Eq.sym 0≈x) y))
+
+x≥0∧y≤0⇒x*y≤0 : ∀ {x y} → x ≥ 0# → y ≤ 0# → x * y ≤ 0#
+x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₁ x>0) (inj₁ y<0) = <⇒≤ (x>0∧y<0⇒x*y<0 x>0 y<0)
+x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₁ x>0) (inj₂ y≈0) = ≤-reflexive (x≈0⇒y*x≈0 y≈0 x)
+x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₂ 0≈x) y≤0        = ≤-reflexive (x≈0⇒x*y≈0 (Eq.sym 0≈x) y)
+
+x≤0∧y≥0⇒x*y≤0 : ∀ {x y} → x ≤ 0# → y ≥ 0# → x * y ≤ 0#
+x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₁ x<0) (inj₁ y>0) = <⇒≤ (x<0∧y>0⇒x*y<0 x<0 y>0)
+x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₁ x<0) (inj₂ 0≈y) = ≤-reflexive (x≈0⇒y*x≈0 (Eq.sym 0≈y) x)
+x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₂ x≈0) y≥0        = ≤-reflexive (x≈0⇒x*y≈0 x≈0 y)
+
+x≤0∧y≤0⇒x*y≥0 : ∀ {x y} → x ≤ 0# → y ≤ 0# → x * y ≥ 0#
+x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₁ x<0) (inj₁ y<0) = <⇒≤ (x<0∧y<0⇒x*y>0 x<0 y<0)
+x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₁ x<0) (inj₂ y≈0) = ≤-reflexive (Eq.sym (x≈0⇒y*x≈0 y≈0 x))
+x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₂ x≈0) y≤0        = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 x≈0 y))
+
+---- Respects signs
+
+-- _<_
+
+-- x>0∧x*y>0⇒y>0
+-- x>0∧x*y<0⇒y<0
+-- x>0∧y*x>0⇒y>0
+-- x>0∧y*x<0⇒y<0
+-- x<0∧x*y>0⇒y<0
+-- x<0∧x*y<0⇒y>0
+-- x<0∧y*x>0⇒y<0
+-- x<0∧y*x<0⇒y>0
+
+-- _≤_
+
+-- x>0∧x*y≥0⇒y≥0
+-- x>0∧x*y≤0⇒y≤0
+-- x>0∧y*x≥0⇒y≥0
+-- x>0∧y*x≤0⇒y≤0
+-- x<0∧x*y≥0⇒y≤0
+-- x<0∧x*y≤0⇒y≥0
+-- x<0∧y*x≥0⇒y≤0
+-- x<0∧y*x≤0⇒y≥0
+
+--------------------------------------------------------------------------------
+---- Properties of 0 and 1
+
+0≤1 : 0# ≤ 1#
+0≤1 = ≮⇒≥ (λ 0>1 → <-asym 0>1 (begin-strict
+  0#      <⟨ x<0∧y<0⇒x*y>0 0>1 0>1 ⟩
+  1# * 1# ≈⟨ *-identity² ⟩
+  1#      ∎))
+
+1≈0⇒x≈y : ∀ {x y} → 1# ≈ 0# → x ≈ y
+1≈0⇒x≈y {x} {y} 1≈0 = begin-equality
+  x      ≈˘⟨ *-identityʳ x ⟩
+  x * 1# ≈⟨  x≈0⇒y*x≈0 1≈0 x ⟩
+  0#     ≈˘⟨ x≈0⇒y*x≈0 1≈0 y ⟩
+  y * 1# ≈⟨  *-identityʳ y ⟩
+  y      ∎
+
+x<y⇒0<1 : ∀ {x y} → x < y → 0# < 1#
+x<y⇒0<1 x<y = ≤∧≉⇒< 0≤1 (<⇒≉ x<y ∘ 1≈0⇒x≈y ∘ Eq.sym)
+
+--------------------------------------------------------------------------------
+---- Properties of _*_ (again)
+
+---- Preserves size
+
+-- _<_
+
+x>1∧y≥1⇒x*y>1 : ∀ {x y} → x > 1# → y ≥ 1# → x * y > 1#
+x>1∧y≥1⇒x*y>1 {x} {y} x>1 y≥1 = begin-strict
+  1#      ≈˘⟨ *-identity² ⟩
+  1# * 1# <⟨  x>0⇒*-monoʳ-< (x<y⇒0<1 x>1) x>1 ⟩
+  x * 1#  ≤⟨  x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 (<⇒≤ x>1)) y≥1 ⟩
+  x * y   ∎
+
+x≥1∧y>1⇒x*y>1 : ∀ {x y} → x ≥ 1# → y > 1# → x * y > 1#
+x≥1∧y>1⇒x*y>1 {x} {y} x≥1 y>1 = begin-strict
+  1#      ≈˘⟨ *-identity² ⟩
+  1# * 1# <⟨  x>0⇒*-monoˡ-< (x<y⇒0<1 y>1) y>1 ⟩
+  1# * y  ≤⟨  x≥0⇒*-monoʳ-≤ (≤-trans 0≤1 (<⇒≤ y>1)) x≥1 ⟩
+  x * y   ∎
+
+0≤x<1∧y≤1⇒x*y<1 : ∀ {x y} → 0# ≤ x → x < 1# → y ≤ 1# → x * y < 1#
+0≤x<1∧y≤1⇒x*y<1 {x} {y} 0≤x x<1 y≤1 = begin-strict
+  x * y   ≤⟨ x≥0⇒*-monoˡ-≤ 0≤x y≤1 ⟩
+  x * 1#  <⟨ x>0⇒*-monoʳ-< (x<y⇒0<1 x<1) x<1 ⟩
+  1# * 1# ≈⟨ *-identity² ⟩
+  1#      ∎
+
+x≤1∧0≤y<1⇒x*y<1 : ∀ {x y} → x ≤ 1# → 0# ≤ y → y < 1# → x * y < 1#
+x≤1∧0≤y<1⇒x*y<1 {x} {y} x≤1 0≤y y<1 = begin-strict
+  x * y   ≤⟨ x≥0⇒*-monoʳ-≤ 0≤y x≤1 ⟩
+  1# * y  <⟨ x>0⇒*-monoˡ-< (x<y⇒0<1 y<1) y<1 ⟩
+  1# * 1# ≈⟨ *-identity² ⟩
+  1#      ∎
+
+-- _≤_
+
+x≥1∧y≥1⇒x*y≥1 : ∀ {x y} → x ≥ 1# → y ≥ 1# → x * y ≥ 1#
+x≥1∧y≥1⇒x*y≥1 {x} {y} x≥1 y≥1 = begin
+  1#      ≈˘⟨ *-identity² ⟩
+  1# * 1# ≤⟨  x≥0⇒*-monoʳ-≤ 0≤1 x≥1 ⟩
+  x * 1#  ≤⟨  x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 x≥1) y≥1 ⟩
+  x * y   ∎
+
+0≤x≤1∧y≤1⇒x*y≤1 : ∀ {x y} → 0# ≤ x → x ≤ 1# → y ≤ 1# → x * y ≤ 1#
+0≤x≤1∧y≤1⇒x*y≤1 {x} {y} 0≤x x≤1 y≤1 = begin
+  x * y   ≤⟨ x≥0⇒*-monoˡ-≤ 0≤x y≤1 ⟩
+  x * 1#  ≤⟨ x≥0⇒*-monoʳ-≤ 0≤1 x≤1 ⟩
+  1# * 1# ≈⟨ *-identity² ⟩
+  1#      ∎
+
+x≤1∧0≤y≤1⇒x*y≤1 : ∀ {x y} → x ≤ 1# → 0# ≤ y → y ≤ 1# → x * y ≤ 1#
+x≤1∧0≤y≤1⇒x*y≤1 {x} {y} x≤1 0≤y y≤1 = begin
+  x * y   ≤⟨ x≥0⇒*-monoʳ-≤ 0≤y x≤1 ⟩
+  1# * y  ≤⟨ x≥0⇒*-monoˡ-≤ 0≤1 y≤1 ⟩
+  1# * 1# ≈⟨ *-identity² ⟩
+  1#      ∎
+
+---- Miscellaneous
+
+x*x≥0 : ∀ x → x * x ≥ 0#
+x*x≥0 x with compare x 0#
+... | tri< x<0 _ _ = <⇒≤ (x<0∧y<0⇒x*y>0 x<0 x<0)
+... | tri≈ _ x≈0 _ = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 x≈0 x))
+... | tri> _ _ x>0 = <⇒≤ (x>0∧y>0⇒x*y>0 x>0 x>0)
+
+--------------------------------------------------------------------------------
+---- Properties of _^_
+
+---- Zero
+
+^-zeroˡ : ∀ n → 1# ^ n ≈ 1#
+^-zeroˡ 0       = Eq.refl
+^-zeroˡ (suc n) = begin-equality
+  1# ^ suc n  ≈⟨ ^-homo-* 1# 1 n ⟩
+  1# * 1# ^ n ≈⟨ *-congˡ (^-zeroˡ n) ⟩
+  1# * 1#     ≈⟨ *-identity² ⟩
+  1#          ∎
+
+^-zeroʳ : ∀ x → x ^ 0 ≈ 1#
+^-zeroʳ x = Eq.refl
+
+---- Identity
+
+^-identityʳ : ∀ x → x ^ 1 ≈ x
+^-identityʳ x = Eq.refl
+
+---- Preserves sign
+
+-- _≤_
+
+x≥0⇒x^n≥0 : ∀ {x} → x ≥ 0# → ∀ n → x ^ n ≥ 0#
+x≥0⇒x^n≥0 {x} x≥0 0       = 0≤1
+x≥0⇒x^n≥0 {x} x≥0 (suc n) = begin
+  0#        ≤⟨  x≥0∧y≥0⇒x*y≥0 x≥0 (x≥0⇒x^n≥0 x≥0 n) ⟩
+  x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n ∎
+
+-- _<_
+
+x>0⇒x^n>0 : ∀ {x} → x > 0# → ∀ n → x ^ n > 0#
+x>0⇒x^n>0 {x} x>0 0       = x<y⇒0<1 x>0
+x>0⇒x^n>0 {x} x>0 (suc n) = begin-strict
+  0#        <⟨  x>0∧y>0⇒x*y>0 x>0 (x>0⇒x^n>0 x>0 n) ⟩
+  x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n ∎
+
+---- Preserves size
+
+-- _≤_
+
+x≥1⇒x^n≥1 : ∀ {x} → x ≥ 1# → ∀ n → x ^ n ≥ 1#
+x≥1⇒x^n≥1 {x} x≥1 0       = ≤-refl
+x≥1⇒x^n≥1 {x} x≥1 (suc n) = begin
+  1#        ≤⟨  x≥1∧y≥1⇒x*y≥1 x≥1 (x≥1⇒x^n≥1 x≥1 n) ⟩
+  x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n ∎
+
+0≤x≤1⇒x^n≤1 : ∀ {x} → 0# ≤ x → x ≤ 1# → ∀ n → x ^ n ≤ 1#
+0≤x≤1⇒x^n≤1 {x} 0≤x x≤1 0       = ≤-refl
+0≤x≤1⇒x^n≤1 {x} 0≤x x≤1 (suc n) = begin
+  x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩
+  x * x ^ n ≤⟨ 0≤x≤1∧y≤1⇒x*y≤1 0≤x x≤1 (0≤x≤1⇒x^n≤1 0≤x x≤1 n) ⟩
+  1#        ∎
+
+-- _<_
+
+x>1∧n≢0⇒x^n>1 : ∀ {x} → x > 1# → ∀ n → ⦃ NonZero n ⦄ → x ^ n > 1#
+x>1∧n≢0⇒x^n>1 {x} x>1 (suc n) = begin-strict
+  1#        <⟨  x>1∧y≥1⇒x*y>1 x>1 (x≥1⇒x^n≥1 (<⇒≤ x>1) n) ⟩
+  x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n ∎
+
+0≤x<1∧n≢0⇒x^n<1 : ∀ {x} → 0# ≤ x → x < 1# → ∀ n → ⦃ NonZero n ⦄ → x ^ n < 1#
+0≤x<1∧n≢0⇒x^n<1 {x} 0≤x x<1 (suc n) = begin-strict
+  x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩
+  x * x ^ n <⟨ 0≤x<1∧y≤1⇒x*y<1 0≤x x<1 (0≤x≤1⇒x^n≤1 0≤x (<⇒≤ x<1) n) ⟩
+  1#        ∎
+
+---- Congruences
+
+-- _≈_
+
+n≢0⇒0^n≈0 : ∀ n → ⦃ NonZero n ⦄ → 0# ^ n ≈ 0#
+n≢0⇒0^n≈0 (suc n) = begin-equality
+  0# ^ suc n  ≈⟨ ^-homo-* 0# 1 n ⟩
+  0# * 0# ^ n ≈⟨ zeroˡ (0# ^ n) ⟩
+  0#          ∎
+
+-- _≤_
+
+x≥1⇒^-monoˡ-≤ : ∀ {x} → x ≥ 1# → (x ^_) Preserves ℕ._≤_ ⟶ _≤_
+x≥1⇒^-monoˡ-≤ {x} x≥1 {.0}     {n}      ℕ.z≤n       = x≥1⇒x^n≥1 x≥1 n
+x≥1⇒^-monoˡ-≤ {x} x≥1 {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin
+  x ^ suc m ≈⟨  ^-homo-* x 1 m ⟩
+  x * x ^ m ≤⟨  x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 x≥1) (x≥1⇒^-monoˡ-≤ x≥1 m≤n) ⟩
+  x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n ∎
+
+0≤x≤1⇒^-anti-monoˡ-≤ : ∀ {x} → 0# ≤ x → x ≤ 1# → (x ^_) Preserves ℕ._≤_ ⟶ _≥_
+0≤x≤1⇒^-anti-monoˡ-≤ {x} 0≤x x≤1 {.0}     {n}      ℕ.z≤n       = 0≤x≤1⇒x^n≤1 0≤x x≤1 n
+0≤x≤1⇒^-anti-monoˡ-≤ {x} 0≤x x≤1 {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin
+  x ^ suc n ≈⟨  ^-homo-* x 1 n ⟩
+  x * x ^ n ≤⟨  x≥0⇒*-monoˡ-≤ 0≤x (0≤x≤1⇒^-anti-monoˡ-≤ 0≤x x≤1 m≤n) ⟩
+  x * x ^ m ≈˘⟨ ^-homo-* x 1 m ⟩
+  x ^ suc m ∎
+
+-- _<_
+
+x>1⇒^-monoˡ-< : ∀ {x} → x > 1# → (x ^_) Preserves ℕ._<_ ⟶ _<_
+x>1⇒^-monoˡ-< {x} x>1 {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict
+  x ^ m      ≤⟨  x≥1⇒^-monoˡ-≤ (<⇒≤ x>1) m≤n ⟩
+  x ^ n      ≈˘⟨ *-identityˡ (x ^ n) ⟩
+  1# * x ^ n <⟨  x>0⇒*-monoʳ-< (x>0⇒x^n>0 (≤-<-trans 0≤1 x>1) n) x>1 ⟩
+  x * x ^ n  ≈˘⟨ ^-homo-* x 1 n ⟩
+  x ^ suc n  ∎
+
+0<x<1⇒^-anti-monoˡ-< : ∀ {x} → 0# < x → x < 1# → (x ^_) Preserves ℕ._<_ ⟶ _>_
+0<x<1⇒^-anti-monoˡ-< {x} 0<x x<1 {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict
+  x ^ suc n  ≈⟨ ^-homo-* x 1 n ⟩
+  x * x ^ n  <⟨ x>0⇒*-monoʳ-< (x>0⇒x^n>0 0<x n) x<1 ⟩
+  1# * x ^ n ≈⟨ *-identityˡ (x ^ n) ⟩
+  x ^ n      ≤⟨ 0≤x≤1⇒^-anti-monoˡ-≤ (<⇒≤ 0<x) (<⇒≤ x<1) m≤n ⟩
+  x ^ m      ∎
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda
new file mode 100644
index 0000000..17228ac
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda
@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered semigroups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup
+  {ℓ₁ ℓ₂ ℓ₃}
+  (semigroup : Semigroup ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Semigroup semigroup
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Magma magma public
+  using
+  ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-<
+  ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤
+  ; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel
+  ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-<
+  ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤
+  )
+open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public