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.

---
 src/Helium/Algebra/Morphism/Structures.agda        |  42 --
 .../Algebra/Ordered/StrictTotal/Bundles.agda       |  46 +-
 .../Algebra/Ordered/StrictTotal/Consequences.agda  | 137 +++++
 .../Ordered/StrictTotal/Morphism/Structures.agda   |  98 ++++
 .../StrictTotal/Properties/AbelianGroup.agda       |  60 ++-
 .../StrictTotal/Properties/CommutativeRing.agda    |  81 ++-
 .../Ordered/StrictTotal/Properties/Group.agda      | 211 +++++++-
 .../Ordered/StrictTotal/Properties/Magma.agda      |  89 ++++
 .../Ordered/StrictTotal/Properties/Monoid.agda     | 329 ++++++++++++
 .../Ordered/StrictTotal/Properties/Ring.agda       | 584 +++++++++++++++++++--
 .../Ordered/StrictTotal/Properties/Semigroup.agda  |  31 ++
 src/Helium/Data/Pseudocode/Algebra.agda            |  28 +-
 src/Helium/Data/Pseudocode/Algebra/Properties.agda | 281 +++++++++-
 .../Binary/Properties/StrictTotalOrder.agda        | 122 +++++
 src/Helium/Semantics/Axiomatic.agda                |  11 +-
 src/Helium/Semantics/Axiomatic/Term.agda           |   4 +-
 src/Helium/Semantics/Denotational/Core.agda        |   6 +-
 17 files changed, 1942 insertions(+), 218 deletions(-)
 delete mode 100644 src/Helium/Algebra/Morphism/Structures.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda
 create mode 100644 src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda

(limited to 'src')

diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda
deleted file mode 100644
index bf219ef..0000000
--- a/src/Helium/Algebra/Morphism/Structures.agda
+++ /dev/null
@@ -1,42 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Redefine Ring monomorphisms to resolve problems with overloading.
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Algebra.Morphism.Structures where
-
-open import Algebra.Bundles using (RawRing)
-open import Algebra.Morphism.Structures
-  hiding (IsRingHomomorphism; module RingMorphisms)
-open import Level using (Level; _⊔_)
-
-private
-  variable
-    a b ℓ₁ ℓ₂ : Level
-
-module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
-  module R₁ = RawRing R₁ renaming (Carrier to A)
-  module R₂ = RawRing R₂ renaming (Carrier to B)
-  open R₁ using (A)
-  open R₂ using (B)
-
-  private
-    module +′ = GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup
-    module *′ = MonoidMorphisms R₁.*-rawMonoid R₂.*-rawMonoid
-
-  record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
-    field
-      +-isGroupHomomorphism  : +′.IsGroupHomomorphism  ⟦_⟧
-      *-isMonoidHomomorphism : *′.IsMonoidHomomorphism ⟦_⟧
-
-    open +′.IsGroupHomomorphism +-isGroupHomomorphism public
-      renaming (homo to +-homo; ε-homo to 0#-homo; ⁻¹-homo to -‿homo)
-
-    open *′.IsMonoidHomomorphism *-isMonoidHomomorphism public
-      hiding (⟦⟧-cong)
-      renaming (homo to *-homo; ε-homo to 1#-homo)
-
-open RingMorphisms public
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
diff --git a/src/Helium/Data/Pseudocode/Algebra.agda b/src/Helium/Data/Pseudocode/Algebra.agda
index 523150d..28a2190 100644
--- a/src/Helium/Data/Pseudocode/Algebra.agda
+++ b/src/Helium/Data/Pseudocode/Algebra.agda
@@ -21,18 +21,20 @@ open import Data.Vec.Functional
 open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
 import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
 open import Function using (_$_; _∘′_; id)
-open import Helium.Algebra.Ordered.StrictTotal.Bundles
 open import Helium.Algebra.Decidable.Bundles
   using (BooleanAlgebra; RawBooleanAlgebra)
 import Helium.Algebra.Decidable.Construct.Pointwise as Pw
-open import Helium.Algebra.Morphism.Structures
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+open import Helium.Algebra.Ordered.StrictTotal.Morphism.Structures
 open import Level using (_⊔_) renaming (suc to ℓsuc)
 open import Relation.Binary.Core using (Rel)
+import Relation.Binary.Construct.StrictToNonStrict as ToNonStrict
 open import Relation.Binary.Definitions
+open import Relation.Binary.Morphism.Structures
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 import Relation.Binary.Reasoning.StrictPartialOrder as Reasoning
 open import Relation.Binary.Structures using (IsStrictTotalOrder)
-open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary using (does; yes; no) renaming (¬_ to ¬′_)
 open import Relation.Nullary.Decidable.Core
   using (False; toWitnessFalse; fromWitnessFalse)
 
@@ -107,21 +109,23 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
   module ℤ-Reasoning = Reasoning ℤ.strictPartialOrder
   module ℝ-Reasoning = Reasoning ℝ.strictPartialOrder
 
+  private
+    module ℤ-ord = ToNonStrict ℤ._≈_ ℤ._<_
+    module ℝ-ord = ToNonStrict ℝ._≈_ ℝ._<_
+
   field
-    integerDiscrete : ∀ x y → y ℤ.≤ x ⊎ x ℤ.+ 1ℤ ℤ.≤ y
-    1≉0 : 1ℤ ℤ.≉ 0ℤ
+    integerDiscrete : ∀ x y → y ℤ-ord.≤ x ⊎ x ℤ.+ 1ℤ ℤ-ord.≤ y
+    1≉0 : ¬′ 1ℤ ℤ.≈ 0ℤ
 
     _/1 : ℤ → ℝ
     ⌊_⌋ : ℝ → ℤ
-    /1-isHomo : IsRingHomomorphism ℤ.Unordered.rawRing ℝ.Unordered.rawRing _/1
-    ⌊⌋-isHomo : IsRingHomomorphism ℝ.Unordered.rawRing ℤ.Unordered.rawRing ⌊_⌋
-    /1-mono-< : ∀ x y → x ℤ.< y → x /1 ℝ.< y /1
-    ⌊⌋-mono-≤ : ∀ x y → x ℝ.≤ y → ⌊ x ⌋ ℤ.≤ ⌊ y ⌋
+    /1-isHomo : IsRingHomomorphism ℤ.rawRing ℝ.rawRing _/1
+    ⌊⌋-isHomo : IsOrderHomomorphism ℝ._≈_ ℤ._≈_ ℝ-ord._≤_ ℤ-ord._≤_ ⌊_⌋
     ⌊⌋-floor : ∀ x y → x ℝ.< y /1 → ⌊ x ⌋ ℤ.< y
-    ⌊⌋∘/1≗id : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x
+    ⌊x/1⌋≈x : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x
 
-  module /1 = IsRingHomomorphism /1-isHomo renaming (⟦⟧-cong to cong)
-  module ⌊⌋ = IsRingHomomorphism ⌊⌋-isHomo renaming (⟦⟧-cong to cong)
+  module /1 = IsRingHomomorphism /1-isHomo
+  module ⌊⌋ = IsOrderHomomorphism ⌊⌋-isHomo
 
   bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂
   bitRawBooleanAlgebra = record
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
index 3ea96be..3c22216 100644
--- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -15,51 +15,288 @@ module Helium.Data.Pseudocode.Algebra.Properties
 
 open import Agda.Builtin.FromNat
 open import Agda.Builtin.FromNeg
+open import Data.Nat using (ℕ; suc; NonZero)
+import Data.Nat.Literals as ℕₗ
+open import Data.Product as × using (∃; _×_; _,_)
+open import Data.Sum using (_⊎_; inj₁; inj₂; map)
+import Data.Unit
+open import Function using (_∘_)
 import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ
-open import Data.Nat using (NonZero)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
+open import Relation.Nullary.Negation using (contradiction)
 
 private
   module pseudocode = Pseudocode pseudocode
+  instance
+    numberℕ : Number ℕ
+    numberℕ = ℕₗ.number
 
 open pseudocode public
   hiding
-  (1≉0; module ℤ; module ℤ′; module ℝ; module ℝ′; module ℤ-Reasoning; module ℝ-Reasoning)
+  ( integerDiscrete; 1≉0; ⌊⌋-floor
+  ; module ℤ; module ℤ′; module ℤ-Reasoning
+  ; module ℝ; module ℝ′; module ℝ-Reasoning
+  ; module ⌊⌋
+  ; module /1
+  )
 
 module ℤ where
-  open pseudocode.ℤ public hiding (ℤ; 0ℤ; 1ℤ)
+  open pseudocode.ℤ public
+    hiding (ℤ; 0ℤ; 1ℤ)
+    renaming
+    ( trans to <-trans
+    ; irrefl to <-irrefl
+    ; asym to <-asym
+    ; 0<a+0<b⇒0<ab to x>0∧y>0⇒xy>0
+    )
   module Reasoning = pseudocode.ℤ-Reasoning
 
   open CommRingₚ integerRing public
-    hiding (1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)
 
-  1≉0 : 1 ≉ 0
-  1≉0 = pseudocode.1≉0
+  discrete : ∀ x y → y ≤ x ⊎ x + 1ℤ ≤ y
+  discrete = pseudocode.integerDiscrete
 
-  n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
-  n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n integerRing 1≉0
+  1≉0 : 1ℤ ≉ 0ℤ
+  1≉0 = pseudocode.1≉0
 
-  n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
-  n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 integerRing 1≉0
+  x≤y<x+1⇒x≈y : ∀ {x y} → x ≤ y → y < x + 1ℤ → x ≈ y
+  x≤y<x+1⇒x≈y {x} {y} x≤y y<x+1 with discrete x y
+  ... | inj₁ y≤x   = ≤-antisym x≤y y≤x
+  ... | inj₂ x+1≤y = contradiction x+1≤y (<⇒≱ y<x+1)
 
 module ℝ where
-  open pseudocode.ℝ public hiding (ℝ; 0ℝ; 1ℝ)
+  open pseudocode.ℝ public
+    hiding (ℝ; 0ℝ; 1ℝ)
+    renaming
+    ( trans to <-trans
+    ; irrefl to <-irrefl
+    ; asym to <-asym
+    ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
+    )
   module Reasoning = pseudocode.ℝ-Reasoning
 
   open CommRingₚ commutativeRing public
     hiding ()
 
-  1≉0 : 1 ≉ 0
+  1≉0 : 1ℝ ≉ 0ℝ
   1≉0 1≈0 = ℤ.1≉0 (begin-equality
-    1        ≈˘⟨ ⌊⌋∘/1≗id 1 ⟩
-    ⌊ 1 /1 ⌋ ≈⟨  ⌊⌋.cong /1.1#-homo ⟩
-    ⌊ 1 ⌋    ≈⟨  ⌊⌋.cong 1≈0 ⟩
-    ⌊ 0 ⌋    ≈˘⟨ ⌊⌋.cong /1.0#-homo ⟩
-    ⌊ 0 /1 ⌋ ≈⟨  ⌊⌋∘/1≗id 0 ⟩
-    0        ∎)
+    1ℤ        ≈˘⟨ ⌊x/1⌋≈x 1ℤ ⟩
+    ⌊ 1ℤ /1 ⌋ ≈⟨  ⌊⌋.cong /1.1#-homo ⟩
+    ⌊ 1ℝ ⌋    ≈⟨  ⌊⌋.cong 1≈0 ⟩
+    ⌊ 0ℝ ⌋    ≈˘⟨ ⌊⌋.cong /1.0#-homo ⟩
+    ⌊ 0ℤ /1 ⌋ ≈⟨  ⌊x/1⌋≈x 0ℤ ⟩
+    0ℤ        ∎)
+    where
+    open ℤ.Reasoning
+    open pseudocode using (module /1; module ⌊⌋)
+
+  x>0⇒x⁻¹>0 : ∀ {x} → (x≉0 : x ≉ 0ℝ) → x > 0ℝ → x≉0 ⁻¹ > 0ℝ
+  x>0⇒x⁻¹>0 {x} x≉0 x>0 = ≰⇒> (λ x⁻¹≤0 → <⇒≱ x>0 (begin
+    x               ≈˘⟨ *-identityˡ x ⟩
+    1ℝ * x          ≈˘⟨ *-congʳ (⁻¹-inverseˡ x≉0) ⟩
+    x≉0 ⁻¹ * x * x  ≤⟨  x≥0⇒*-monoʳ-≤ (<⇒≤ x>0) (x≤0⇒*-anti-monoˡ-≤ x⁻¹≤0 (<⇒≤ x>0)) ⟩
+    x≉0 ⁻¹ * 0ℝ * x ≈⟨  *-congʳ (zeroʳ (x≉0 ⁻¹)) ⟩
+    0ℝ * x          ≈⟨  zeroˡ x ⟩
+    0ℝ              ∎))
+    where open Reasoning
+
+  record IsMonotoneContinuous (f : ℝ → ℝ) : Set (r₁ ⊔ r₂ ⊔ r₃) where
+    field
+      cong : f Preserves _≈_ ⟶ _≈_
+      mono-≤ : f Preserves _≤_ ⟶ _≤_
+      continuous-≤-< : ∀ {x y z} → f x ≤ z → z < f y → ∃ λ α → f α ≈ z × x ≤ α × α < y
+      continuous-<-≤ : ∀ {x y z} → f x < z → z ≤ f y → ∃ λ α → f α ≈ z × x < α × α ≤ y
+      continuous-<-< : ∀ {x y z} → f x < z → z < f y → ∃ λ α → f α ≈ z × x < α × α < y
+
+  record MCHelper (f : ℝ → ℝ) : Set (r₁ ⊔ r₂ ⊔ r₃) where
+    field
+      cong : f Preserves _≈_ ⟶ _≈_
+      mono-≤ : f Preserves _≤_ ⟶ _≤_
+      continuous-<-< : ∀ {x y z} → f x < z → z < f y → ∃ λ α → f α ≈ z × x < α × α < y
+
+  mcHelper : ∀ {f} → MCHelper f → IsMonotoneContinuous f
+  mcHelper {f} helper = record
+    { cong = cong
+    ; mono-≤ = mono-≤
+    ; continuous-≤-< = continuous-≤-<
+    ; continuous-<-≤ = continuous-<-≤
+    ; continuous-<-< = continuous-<-<
+    }
+    where
+    open MCHelper helper
+    cancel-< : ∀ {x y} → f x < f y → x < y
+    cancel-< fx<fy = ≰⇒> (<⇒≱ fx<fy ∘ mono-≤)
+
+    continuous-≤-< : ∀ {x y z} → f x ≤ z → z < f y → ∃ λ α → f α ≈ z × x ≤ α × α < y
+    continuous-≤-< {x} {y} {z} (inj₁ fx<z) z<fy with continuous-<-< fx<z z<fy
+    ... | α , fα≈z , x<α , α<y = α , fα≈z , inj₁ x<α , α<y
+    continuous-≤-< {x} {y} {z} (inj₂ fx≈z) z<fy = x , fx≈z , inj₂ Eq.refl , cancel-< (<-respˡ-≈ (Eq.sym fx≈z) z<fy)
+
+    continuous-<-≤ : ∀ {x y z} → f x < z → z ≤ f y → ∃ λ α → f α ≈ z × x < α × α ≤ y
+    continuous-<-≤ {x} {y} {z} fx<z (inj₁ z<fy) with continuous-<-< fx<z z<fy
+    ... | α , fα≈z , x<α , α<y = α , fα≈z , x<α , inj₁ α<y
+    continuous-<-≤ {x} {y} {z} fx<z (inj₂ z≈fy) = y , Eq.sym z≈fy , cancel-< (<-respʳ-≈ z≈fy fx<z) , inj₂ Eq.refl
+
+  -- FIXME: bikeshed
+  record IntegerPreimage (f : ℝ → ℝ) : Set (i₁ ⊔ r₁ ⊔ r₂) where
+    field
+      g        : ℤ → ℤ
+      preimage : ∀ {x y} → f y ≈ x /1 → g x /1 ≈ y
+
+module /1 where
+  open pseudocode./1 public
+    renaming
+      (mono to mono-<)
+
+  mono-≤ : ∀ {x y} → x ℤ.≤ y → x /1 ℝ.≤ y /1
+  mono-≤ = map mono-< cong
+
+  cancel-< : ∀ {x y} → x /1 ℝ.< y /1 → x ℤ.< y
+  cancel-< {x} {y} x<y = ℤ.≤∧≉⇒<
+    (begin
+      x        ≈˘⟨ ⌊x/1⌋≈x x ⟩
+      ⌊ x /1 ⌋ ≤⟨  pseudocode.⌊⌋.mono (ℝ.<⇒≤ x<y) ⟩
+      ⌊ y /1 ⌋ ≈⟨  ⌊x/1⌋≈x y ⟩
+      y        ∎)
+    (ℝ.<⇒≉ x<y ∘ cong)
+    where open ℤ.Reasoning
+
+  cancel-≤ : ∀ {x y} → x /1 ℝ.≤ y /1 → x ℤ.≤ y
+  cancel-≤ {x} {y} x≤y = begin
+      x        ≈˘⟨ ⌊x/1⌋≈x x ⟩
+      ⌊ x /1 ⌋ ≤⟨  pseudocode.⌊⌋.mono x≤y ⟩
+      ⌊ y /1 ⌋ ≈⟨  ⌊x/1⌋≈x y ⟩
+      y        ∎
+    where open ℤ.Reasoning
+
+module ⌊⌋ where
+  open pseudocode.⌊⌋ public
+    renaming
+      (mono to mono-≤)
+
+  cancel-< : ∀ {x y} → ⌊ x ⌋ ℤ.< ⌊ y ⌋ → x ℝ.< y
+  cancel-< {x} {y} ⌊x⌋<⌊y⌋ = ℝ.≰⇒> (λ x≥y → ℤ.<⇒≱ ⌊x⌋<⌊y⌋ (mono-≤ x≥y))
+
+  floor : ∀ {x y} → x ℝ.< y /1 → ⌊ x ⌋ ℤ.< y
+  floor {x} {y} = pseudocode.⌊⌋-floor x y
+
+  n≤x⇒n≤⌊x⌋ : ∀ {n x} → n /1 ℝ.≤ x → n ℤ.≤ ⌊ x ⌋
+  n≤x⇒n≤⌊x⌋ {n} {x} n≤x = begin
+    n       ≈˘⟨ ⌊x/1⌋≈x n ⟩
+    ⌊ n /1 ⌋ ≤⟨  mono-≤ n≤x ⟩
+    ⌊ x ⌋    ∎
+    where open ℤ.Reasoning
+
+  ⌊x⌋≤x : ∀ x → ⌊ x ⌋ /1 ℝ.≤ x
+  ⌊x⌋≤x x = ℝ.≮⇒≥ (λ x<⌊x⌋ → ℤ.<-asym (floor x<⌊x⌋) (floor x<⌊x⌋))
+
+  x<⌊x⌋+1 : ∀ x → x ℝ.< (⌊ x ⌋ ℤ.+ 1ℤ) /1
+  x<⌊x⌋+1 x = ℝ.≰⇒> (λ x≥⌊x⌋+1 → ℤ.<⇒≱ (ℤ.≤∧≉⇒< ℤ.0≤1 (ℤ.1≉0 ∘ ℤ.Eq.sym)) (ℤ.+-cancelˡ-≤ ⌊ x ⌋ (begin
+    ⌊ x ⌋ ℤ.+ 1ℤ ≤⟨  n≤x⇒n≤⌊x⌋ x≥⌊x⌋+1 ⟩
+    ⌊ x ⌋        ≈˘⟨ ℤ.+-identityʳ ⌊ x ⌋ ⟩
+    ⌊ x ⌋ ℤ.+ 0ℤ ∎)))
+    where open ℤ.Reasoning
+
+  n≤x<n+1⇒n≈⌊x⌋ : ∀ {n x} → n /1 ℝ.≤ x → x ℝ.< n /1 ℝ.+ 1ℝ → n ℤ.≈ ⌊ x ⌋
+  n≤x<n+1⇒n≈⌊x⌋ {n} {x} n≤x x<n+1 = begin-equality
+    n       ≈˘⟨ ⌊x/1⌋≈x n ⟩
+    ⌊ n /1 ⌋ ≈⟨  ℤ.x≤y<x+1⇒x≈y (mono-≤ n≤x) (floor x<[⌊n/1⌋+1]/1) ⟩
+    ⌊ x ⌋    ∎
+    where
+    x<[⌊n/1⌋+1]/1 = begin-strict
+      x                     <⟨  x<n+1 ⟩
+      n /1 ℝ.+ 1ℝ           ≈˘⟨ ℝ.+-cong (/1.cong (⌊x/1⌋≈x n)) /1.1#-homo ⟩
+      ⌊ n /1 ⌋ /1 ℝ.+ 1ℤ /1 ≈˘⟨ /1.+-homo ⌊ n /1 ⌋ 1ℤ ⟩
+      (⌊ n /1 ⌋ ℤ.+ 1ℤ) /1  ∎
+      where open ℝ.Reasoning
+    open ℤ.Reasoning
+
+  ⌊x+n⌋≈⌊x⌋+n : ∀ x n → ⌊ x ℝ.+ n /1 ⌋ ℤ.≈ ⌊ x ⌋ ℤ.+ n
+  ⌊x+n⌋≈⌊x⌋+n x n = ℤ.Eq.sym (n≤x<n+1⇒n≈⌊x⌋ ⌊x⌋+n≤x+n x+n<⌊x⌋+n+1)
+    where
+    open ℝ.Reasoning
+    ⌊x⌋+n≤x+n = begin
+      (⌊ x ⌋ ℤ.+ n) /1  ≈⟨ /1.+-homo ⌊ x ⌋ n ⟩
+      ⌊ x ⌋ /1 ℝ.+ n /1 ≤⟨ ℝ.+-monoʳ-≤ (⌊x⌋≤x x) ⟩
+      x ℝ.+ n /1       ∎
+
+    x+n<⌊x⌋+n+1 = begin-strict
+      x ℝ.+ n /1                 <⟨  ℝ.+-monoʳ-< (x<⌊x⌋+1 x) ⟩
+      (⌊ x ⌋ ℤ.+ 1ℤ) /1 ℝ.+ n /1   ≈⟨  ℝ.+-congʳ (/1.+-homo ⌊ x ⌋ 1ℤ) ⟩
+      ⌊ x ⌋ /1 ℝ.+ 1ℤ /1 ℝ.+ n /1  ≈⟨  ℝ.+-congʳ (ℝ.+-congˡ /1.1#-homo) ⟩
+      ⌊ x ⌋ /1 ℝ.+ 1ℝ ℝ.+ n /1     ≈⟨  ℝ.+-assoc (⌊ x ⌋ /1) 1ℝ (n /1) ⟩
+      ⌊ x ⌋ /1 ℝ.+ (1ℝ ℝ.+ n /1)   ≈⟨  ℝ.+-congˡ (ℝ.+-comm 1ℝ (n /1)) ⟩
+      ⌊ x ⌋ /1 ℝ.+ (n /1 ℝ.+ 1ℝ)   ≈˘⟨ ℝ.+-assoc (⌊ x ⌋ /1) (n /1) 1ℝ ⟩
+      ⌊ x ⌋ /1 ℝ.+ n /1 ℝ.+ 1ℝ     ≈˘⟨ ℝ.+-congʳ (/1.+-homo ⌊ x ⌋ n) ⟩
+      (⌊ x ⌋ ℤ.+ n) /1 ℝ.+ 1ℝ      ∎
+
+  ⌊x⌋+⌊y⌋≤⌊x+y⌋ : ∀ x y → ⌊ x ⌋ ℤ.+ ⌊ y ⌋ ℤ.≤ ⌊ x ℝ.+ y ⌋
+  ⌊x⌋+⌊y⌋≤⌊x+y⌋ x y = begin
+    ⌊ x ⌋ ℤ.+ ⌊ y ⌋    ≈˘⟨ ⌊x+n⌋≈⌊x⌋+n x ⌊ y ⌋ ⟩
+    ⌊ x ℝ.+ ⌊ y ⌋ /1 ⌋ ≤⟨  mono-≤ (ℝ.+-monoˡ-≤ (⌊x⌋≤x y)) ⟩
+    ⌊ x ℝ.+ y ⌋        ∎
     where open ℤ.Reasoning
 
-  n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
-  n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n commutativeRing 1≉0
+  ⌊x+y⌋≤⌊x⌋+⌊y⌋+1 : ∀ x y → ⌊ x ℝ.+ y ⌋ ℤ.≤ ⌊ x ⌋ ℤ.+ ⌊ y ⌋ ℤ.+ 1ℤ
+  ⌊x+y⌋≤⌊x⌋+⌊y⌋+1 x y = begin
+    ⌊ x ℝ.+ y ⌋                 ≤⟨  mono-≤ (ℝ.+-monoˡ-≤ (ℝ.<⇒≤ (x<⌊x⌋+1 y))) ⟩
+    ⌊ x ℝ.+ (⌊ y ⌋ ℤ.+ 1ℤ) /1 ⌋ ≈⟨  ⌊x+n⌋≈⌊x⌋+n x (⌊ y ⌋ ℤ.+ 1ℤ) ⟩
+    ⌊ x ⌋ ℤ.+ (⌊ y ⌋ ℤ.+ 1ℤ)    ≈˘⟨ ℤ.+-assoc ⌊ x ⌋ ⌊ y ⌋ 1ℤ ⟩
+    ⌊ x ⌋ ℤ.+ ⌊ y ⌋ ℤ.+ 1ℤ      ∎
+    where open ℤ.Reasoning
+
+  -- ⌊⌊x⌋+m/n⌋≈⌊x+m/n⌋ : ∀ x m {n} → (n>0 : n ℤ.> 0) →
+  --   let n≉0 = ℤ.<⇒≉ n>0 ∘ ℤ.Eq.sym in
+  --   ⌊ ⌊ x ⌋ /1 ℝ.* m /1 ℝ.* n≉0 ℤ.⁻¹ ⌋ ℤ.≈ ⌊ x ℝ.* m /1 ℝ.* n≉0 ℤ.⁻¹ ⌋
+  -- ⌊⌊x⌋+m/n⌋≈⌊x+m/n⌋ x m {n} n>0 = ℤ.≤∧≮⇒≈ {!!} {!!}
+
+  f-monocont+int-preimage⇒⌊f⌊x⌋⌋≈⌊fx⌋  :
+    ∀ (f : ℝ → ℝ) → ℝ.IsMonotoneContinuous f → ℝ.IntegerPreimage f →
+    ∀ x → ⌊ f (⌊ x ⌋ /1) ⌋ ℤ.≈ ⌊ f x ⌋
+  f-monocont+int-preimage⇒⌊f⌊x⌋⌋≈⌊fx⌋ f cont int-preimage x =
+    ℤ.≤∧≮⇒≈ (mono-≤ (cont.mono-≤ (⌊x⌋≤x x))) (×.uncurry ¬helper ∘ ×.proj₂ ∘ helper)
+    where
+    module cont = ℝ.IsMonotoneContinuous cont
+    module int-preimage = ℝ.IntegerPreimage int-preimage
+
+    helper : ⌊ f (⌊ x ⌋ /1) ⌋ ℤ.< ⌊ f x ⌋ → ∃ λ y → ⌊ x ⌋ ℤ.< y × y /1 ℝ.≤ x
+    helper f⌊x⌋<fx = b , /1.cancel-< ⌊x⌋<b , b≤x
+      where
+      f⌊x⌋<⌊fx⌋ = cancel-< (begin-strict
+        ⌊ f (⌊ x ⌋ /1) ⌋ <⟨  f⌊x⌋<fx ⟩
+        ⌊ f x ⌋          ≈˘⟨ ⌊x/1⌋≈x ⌊ f x ⌋ ⟩
+        ⌊ ⌊ f x ⌋ /1 ⌋   ∎)
+        where open ℤ.Reasoning
+      a = cont.continuous-<-≤ f⌊x⌋<⌊fx⌋ (⌊x⌋≤x (f x))
+      b  = int-preimage.g ⌊ f x ⌋
+      b≈a = int-preimage.preimage (×.proj₁ (×.proj₂ a))
+      ⌊x⌋<b = begin-strict
+        ⌊ x ⌋ /1     <⟨  ×.proj₁ (×.proj₂ (×.proj₂ a)) ⟩
+        ×.proj₁ a    ≈˘⟨ b≈a ⟩
+        b /1         ∎
+        where open ℝ.Reasoning
+
+      b≤x = begin
+        b /1         ≈⟨ b≈a ⟩
+        ×.proj₁ a    ≤⟨ ×.proj₂ (×.proj₂ (×.proj₂ a)) ⟩
+        x            ∎
+        where open ℝ.Reasoning
 
-  n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
-  n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 commutativeRing 1≉0
+    ¬helper : ∀ {y} → ⌊ x ⌋ ℤ.< y → y /1 ℝ.≰ x
+    ¬helper {y} x<y = ℤ.<⇒≱ x<y ∘ ℤ.≤-respˡ-≈ (⌊x/1⌋≈x y) ∘ mono-≤
+
+  0#-homo : ⌊ 0ℝ ⌋ ℤ.≈ 0ℤ
+  0#-homo = begin-equality
+    ⌊ 0ℝ ⌋    ≈˘⟨ cong /1.0#-homo ⟩
+    ⌊ 0ℤ /1 ⌋ ≈⟨  ⌊x/1⌋≈x 0ℤ ⟩
+    0ℤ       ∎
+    where open ℤ.Reasoning
+
+  1#-homo : ⌊ 1ℝ ⌋ ℤ.≈ 1ℤ
+  1#-homo = begin-equality
+    ⌊ 1ℝ ⌋    ≈˘⟨ cong /1.1#-homo ⟩
+    ⌊ 1ℤ /1 ⌋ ≈⟨  ⌊x/1⌋≈x 1ℤ ⟩
+    1ℤ       ∎
+    where open ℤ.Reasoning
diff --git a/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda
new file mode 100644
index 0000000..43f001c
--- /dev/null
+++ b/src/Helium/Relation/Binary/Properties/StrictTotalOrder.agda
@@ -0,0 +1,122 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Relational properties of strict total orders
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary
+
+module Helium.Relation.Binary.Properties.StrictTotalOrder
+  {a ℓ₁ ℓ₂} (STO : StrictTotalOrder a ℓ₁ ℓ₂)
+  where
+
+open import Data.Sum using (inj₁; inj₂)
+open import Function using (flip)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
+
+open StrictTotalOrder STO
+  renaming
+  ( trans to <-trans
+  ; irrefl to <-irrefl
+  ; asym to <-asym
+  )
+
+import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as ToNonStrict
+
+infix 4 _≉_ _≮_ _≤_ _≰_ _>_ _≥_
+
+_≉_ : Rel Carrier ℓ₁
+x ≉ y = ¬ x ≈ y
+
+_≮_ : Rel Carrier ℓ₂
+x ≮ y = ¬ x < y
+
+_≤_ : Rel Carrier _
+_≤_ = ToNonStrict._≤_
+
+_≰_ : Rel Carrier _
+x ≰ y = ¬ x ≤ y
+
+_>_ : Rel Carrier ℓ₂
+_>_ = flip _<_
+
+_≥_ : Rel Carrier _
+_≥_ = flip _≤_
+
+
+<-≤-trans : Trans _<_ _≤_ _<_
+<-≤-trans = ToNonStrict.<-≤-trans <-trans <-respʳ-≈
+
+≤-<-trans : Trans _≤_ _<_ _<_
+≤-<-trans = ToNonStrict.≤-<-trans Eq.sym <-trans <-respˡ-≈
+
+
+≤-respˡ-≈ : _≤_ Respectsˡ _≈_
+≤-respˡ-≈ = ToNonStrict.≤-respˡ-≈ Eq.sym Eq.trans <-respˡ-≈
+
+≤-respʳ-≈ : _≤_ Respectsʳ _≈_
+≤-respʳ-≈ = ToNonStrict.≤-respʳ-≈ Eq.trans <-respʳ-≈
+
+≤-resp-≈ : _≤_ Respects₂ _≈_
+≤-resp-≈ = ToNonStrict.≤-resp-≈ Eq.isEquivalence <-resp-≈
+
+≤-reflexive : _≈_ ⇒ _≤_
+≤-reflexive = ToNonStrict.reflexive
+
+≤-refl : Reflexive _≤_
+≤-refl = ≤-reflexive Eq.refl
+
+≤-trans : Transitive _≤_
+≤-trans = ToNonStrict.trans Eq.isEquivalence <-resp-≈ <-trans
+
+≤-antisym : Antisymmetric _≈_ _≤_
+≤-antisym = ToNonStrict.antisym Eq.isEquivalence <-trans <-irrefl
+
+≤-total : Total _≤_
+≤-total = ToNonStrict.total compare
+
+
+<⇒≤ : _<_ ⇒ _≤_
+<⇒≤ = ToNonStrict.<⇒≤
+
+<⇒≉ : Irreflexive _<_ _≈_
+<⇒≉ = flip <-irrefl
+
+≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
+≤∧≉⇒< (inj₁ x<y) x≉y = x<y
+≤∧≉⇒< (inj₂ x≈y) x≉y = contradiction x≈y x≉y
+
+
+≤∧≮⇒≈ : ∀ {x y} → x ≤ y → x ≮ y → x ≈ y
+≤∧≮⇒≈ (inj₁ x<y) x≮y = contradiction x<y x≮y
+≤∧≮⇒≈ (inj₂ x≈y) x≮y = x≈y
+
+
+<⇒≱ : Irreflexive _<_ _≥_
+<⇒≱ x<y (inj₁ x>y) = <-asym x<y x>y
+<⇒≱ x<y (inj₂ y≈x) = <-irrefl (Eq.sym y≈x) x<y
+
+≰⇒> : _≰_ ⇒ _>_
+≰⇒> {x} {y} x≰y with compare x y
+... | tri< x<y _ _ = contradiction (<⇒≤ x<y) x≰y
+... | tri≈ _ x≈y _ = contradiction (≤-reflexive x≈y) x≰y
+... | tri> _ _ x>y = x>y
+
+
+≤⇒≯ : Irreflexive _≤_ _>_
+≤⇒≯ = flip <⇒≱
+
+≮⇒≥ : _≮_ ⇒ _≥_
+≮⇒≥ {x} {y} x≮y with compare x y
+... | tri< x<y _ _ = contradiction x<y x≮y
+... | tri≈ _ x≈y _ = ≤-reflexive (Eq.sym x≈y)
+... | tri> _ _ x>y = <⇒≤ x>y
+
+≮∧≯⇒≈ : ∀ {x y} → x ≮ y → y ≮ x → x ≈ y
+≮∧≯⇒≈ {x} {y} x≮y x≯y with compare x y
+... | tri< x<y _ _ = contradiction x<y x≮y
+... | tri≈ _ x≈y _ = x≈y
+... | tri> _ _ x>y = contradiction x>y x≯y
diff --git a/src/Helium/Semantics/Axiomatic.agda b/src/Helium/Semantics/Axiomatic.agda
index dfac609..2fa3db1 100644
--- a/src/Helium/Semantics/Axiomatic.agda
+++ b/src/Helium/Semantics/Axiomatic.agda
@@ -15,11 +15,10 @@ module Helium.Semantics.Axiomatic
 
 open import Helium.Data.Pseudocode.Algebra.Properties pseudocode
 
-open import Agda.Builtin.FromNat
 open import Data.Nat using (ℕ)
-import Data.Nat.Literals as ℕₗ
 import Data.Unit
 open import Data.Vec using (Vec)
+open import Function using (_∘_)
 open import Helium.Data.Pseudocode.Core
 import Helium.Semantics.Axiomatic.Core rawPseudocode as Core
 import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion
@@ -36,12 +35,8 @@ open Term.Term public
 open Term public
   using (Term)
 
-instance
-  numberℕ : Number ℕ
-  numberℕ = ℕₗ.number
-
-2≉0 : 2 ℝ.≉ 0
-2≉0 = ℝ.>⇒≉ (ℝ.n≉0⇒0<+n 2)
+2≉0 : 2 ℝ.× 1ℝ ℝ.≉ 0ℝ
+2≉0 = ℝ.<⇒≉ (ℝ.n≢0∧x>0⇒n×x>0 2 (ℝ.≤∧≉⇒< ℝ.0≤1 (ℝ.1≉0 ∘ ℝ.Eq.sym))) ∘ ℝ.Eq.sym
 
 HoareTriple : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} → Assertion Σ Γ Δ → Code.Statement Σ Γ → Assertion Σ Γ Δ → Set _
 HoareTriple = Triple.HoareTriple 2≉0
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index eaefb89..c9ddd02 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -32,7 +32,7 @@ import Helium.Data.Pseudocode.Manipulate as M
 open import Helium.Semantics.Axiomatic.Core rawPseudocode
 open import Level using (_⊔_; lift; lower)
 open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
-open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Nullary.Negation using (contradiction)
 
@@ -216,7 +216,7 @@ cast τ eq = func₁ (cast′ τ eq)
 [ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
 
 2≉0 : Set _
-2≉0 = 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
 
 [_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
 [ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 090e0ba..07c71bd 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -33,7 +33,7 @@ import Induction as I
 import Induction.WellFounded as Wf
 open import Level using (Level; _⊔_; 0ℓ)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
-open import Relation.Nullary using (does)
+open import Relation.Nullary using (does) renaming (¬_ to ¬′_)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
 
 ⟦_⟧ₗ : Type → Level
@@ -196,12 +196,12 @@ pow : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
 pow int  x n = x ℤ′.^′ n
 pow real x n = x ℝ′.^′ n
 
-shiftr : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
+shiftr : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ → ⟦ int ⟧ₜ → ℕ → ⟦ int ⟧ₜ
 shiftr 2≉0 x n = ⌊ x /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
 
 module Expression
   {o} {Σ : Vec Type o}
-  (2≉0 : 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ)
+  (2≉0 : ¬′ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ)
   where
 
   open Code Σ
-- 
cgit v1.2.3