1 files changed, 81 insertions, 0 deletions
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
new file mode 100644
index 0000000..484143c
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Ring
+  {ℓ₁ ℓ₂ ℓ₃}
+  (ring : Ring ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Ring ring
+
+open import Agda.Builtin.FromNat
+open import Agda.Builtin.FromNeg
+open import Data.Nat 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 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.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelianGroup public
+  using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>)
+  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           ∎