Add some more algebraic properties.

3 files changed, 40 insertions, 2 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index 3915f07..4469c03 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -199,6 +199,16 @@ y>0∧x<y⇒x*y⁻¹<1 {x} {y} y>0 x<y = x≥0⇒*-cancelʳ-< (<⇒≤ y>0) (beg
   1# * y           ∎)
   where y≉0 = <⇒≉ y>0 ∘ Eq.sym
 
+y>0∧x≤y⇒x*y⁻¹≤1 : ∀ {x y} (y>0 : y > 0#) → x ≤ y → x * (<⇒≉ y>0 ∘ Eq.sym) ⁻¹ ≤ 1#
+y>0∧x≤y⇒x*y⁻¹≤1 {x} {y} y>0 x≤y = x>0⇒*-cancelʳ-≤ y>0 (begin
+  x * y≉0 ⁻¹ * y   ≈⟨  *-assoc x _ y ⟩
+  x * (y≉0 ⁻¹ * y) ≈⟨  *-congˡ (⁻¹-inverseˡ y≉0) ⟩
+  x * 1#           ≈⟨  *-identityʳ x ⟩
+  x                ≤⟨  x≤y ⟩
+  y                ≈˘⟨ *-identityˡ y ⟩
+  1# * y           ∎)
+  where y≉0 = <⇒≉ y>0 ∘ Eq.sym
+
 --------------------------------------------------------------------------------
 ---- Properties of -_ and _⁻¹
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
index 79d3b2d..eb46e27 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -126,7 +126,7 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
 
   ; -‿⁻¹-comm
   ; x≉0⇒x⁻¹≉0
-  ; y>0∧x<y⇒x*y⁻¹<1
+  ; y>0∧x<y⇒x*y⁻¹<1; y>0∧x≤y⇒x*y⁻¹≤1
   )
 
 --------------------------------------------------------------------------------
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
index 39bd1e7..22bc0a2 100644
--- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -20,7 +20,7 @@ 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 (_∘_)
+open import Function using (_∘_; Injective)
 import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ
 import Helium.Algebra.Ordered.StrictTotal.Properties.Field as Fieldₚ
 open import Level using (_⊔_)
@@ -144,6 +144,14 @@ module /1 where
   mono-≤ : ∀ {x y} → x ℤ.≤ y → x /1 ℝ.≤ y /1
   mono-≤ = map mono-< cong
 
+  injective : Injective ℤ._≈_ ℝ._≈_ _/1
+  injective {x} {y} x≈y = begin-equality
+    x        ≈˘⟨ ⌊x/1⌋≈x x ⟩
+    ⌊ x /1 ⌋ ≈⟨  pseudocode.⌊⌋.cong x≈y ⟩
+    ⌊ y /1 ⌋ ≈⟨  ⌊x/1⌋≈x y ⟩
+    y        ∎
+    where open ℤ.Reasoning
+
   cancel-< : ∀ {x y} → x /1 ℝ.< y /1 → x ℤ.< y
   cancel-< {x} {y} x<y = ℤ.≤∧≉⇒<
     (begin
@@ -162,6 +170,26 @@ module /1 where
       y        ∎
     where open ℤ.Reasoning
 
+  ×-homo : ∀ n x → (n ℤ.× x) /1 ℝ.≈ n ℝ.× x /1
+  ×-homo 0       x = 0#-homo
+  ×-homo (suc n) x = begin-equality
+    (suc n ℤ.× x) /1      ≈⟨  cong (ℤ.1+× n x) ⟩
+    (x ℤ.+ n ℤ.× x) /1    ≈⟨  +-homo x _ ⟩
+    x /1 ℝ.+ (n ℤ.× x) /1 ≈⟨  ℝ.+-congˡ (×-homo n x) ⟩
+    x /1 ℝ.+ n ℝ.× x /1   ≈˘⟨ ℝ.1+× n (x /1) ⟩
+    suc n ℝ.× x /1        ∎
+    where open ℝ.Reasoning
+
+  ^-homo : ∀ x n → (x ℤ.^ n) /1 ℝ.≈ x /1 ℝ.^ n
+  ^-homo x 0       = 1#-homo
+  ^-homo x (suc n) = begin-equality
+    (x ℤ.^ suc n) /1      ≈⟨  cong (ℤ.^-homo-* x 1 n) ⟩
+    (x ℤ.* x ℤ.^ n) /1    ≈⟨  *-homo x _ ⟩
+    x /1 ℝ.* (x ℤ.^ n) /1 ≈⟨  ℝ.*-congˡ (^-homo x n) ⟩
+    x /1 ℝ.* (x /1) ℝ.^ n ≈˘⟨ ℝ.^-homo-* (x /1) 1 n ⟩
+    x /1 ℝ.^ suc n        ∎
+    where open ℝ.Reasoning
+
 module ⌊⌋ where
   open pseudocode.⌊⌋ public
     renaming