From b212c150ec0a9bf45cf6c28fba997693669e78d2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 5 Apr 2022 12:06:33 +0100
Subject: Minor clean up.

---
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda | 10 +++++-----
 src/Helium/Data/Pseudocode/Algebra/Properties.agda           |  5 -----
 2 files changed, 5 insertions(+), 10 deletions(-)

(limited to 'src')

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
index e186c71..5cf2d5b 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -202,14 +202,14 @@ x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x⁻¹
 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 ⟩
+  x ∙ x ⁻¹ <⟨  ∙-monoʳ-< 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 ⟩
+  ε ∙ x          <⟨  ∙-monoʳ-< ε<yx⁻¹ ⟩
+  y ∙ x ⁻¹ ∙ x   ≈⟨  assoc y (x ⁻¹) x ⟩
+  y ∙ (x ⁻¹ ∙ x) ≈⟨  ∙-congˡ (inverseˡ x) ⟩
+  y ∙ ε          ≈⟨  identityʳ y ⟩
   y              ∎
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
index 1c52cda..39bd1e7 100644
--- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -238,11 +238,6 @@ module ⌊⌋ where
     ⌊ 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 ⌋
-- 
cgit v1.2.3