Add more properties for ordered structures.

2 files changed, 275 insertions, 34 deletions

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