diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 89aa81501e..662f2615dc 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -9,6 +9,7 @@
 ```agda
 module elementary-number-theory where
 
+open import elementary-number-theory.absolute-value-closed-intervals-rational-numbers public
 open import elementary-number-theory.absolute-value-integers public
 open import elementary-number-theory.absolute-value-rational-numbers public
 open import elementary-number-theory.ackermann-function public
@@ -115,6 +116,7 @@ open import elementary-number-theory.kolakoski-sequence public
 open import elementary-number-theory.legendre-symbol public
 open import elementary-number-theory.lower-bounds-natural-numbers public
 open import elementary-number-theory.maximum-natural-numbers public
+open import elementary-number-theory.maximum-nonnegative-rational-numbers public
 open import elementary-number-theory.maximum-positive-rational-numbers public
 open import elementary-number-theory.maximum-rational-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
diff --git a/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md
new file mode 100644
index 0000000000..21651d39f0
--- /dev/null
+++ b/src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md
@@ -0,0 +1,88 @@
+# Absolute value on closed intervals in the rational numbers
+
+```agda
+module elementary-number-theory.absolute-value-closed-intervals-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.inequality-nonnegative-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-nonnegative-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.binary-transport
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+The
+[absolute value](elementary-number-theory.absolute-value-rational-numbers.md) of
+an element of a
+[closed interval](elementary-number-theory.closed-intervals-rational-numbers.md)
+`[a, b]` of [rational numbers](elementary-number-theory.rational-numbers.md) is
+bounded by `max(|a|, |b|)`.
+
+## Definition
+
+```agda
+max-abs-closed-interval-ℚ : closed-interval-ℚ → ℚ⁰⁺
+max-abs-closed-interval-ℚ ((p , q) , p≤q) = max-ℚ⁰⁺ (abs-ℚ p) (abs-ℚ q)
+
+rational-max-abs-closed-interval-ℚ : closed-interval-ℚ → ℚ
+rational-max-abs-closed-interval-ℚ [p,q] =
+  rational-ℚ⁰⁺ (max-abs-closed-interval-ℚ [p,q])
+```
+
+## Properties
+
+### If `r ∈ [p,q]`, then `|r| ≤ max(|p|, |q|)`
+
+```agda
+abstract
+  leq-max-abs-is-in-closed-interval-ℚ :
+    ([p,q] : closed-interval-ℚ) (r : ℚ) → is-in-closed-interval-ℚ [p,q] r →
+    leq-ℚ⁰⁺ (abs-ℚ r) (max-abs-closed-interval-ℚ [p,q])
+  leq-max-abs-is-in-closed-interval-ℚ ((p , q) , p≤q) r (p≤r , r≤q) =
+    rec-coproduct
+      ( λ r≤0 →
+        transitive-leq-ℚ
+          ( rational-abs-ℚ r)
+          ( rational-abs-ℚ p)
+          ( max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+          ( leq-left-max-ℚ _ _)
+          ( leq-abs-leq-leq-neg-ℚ
+            ( r)
+            ( rational-abs-ℚ p)
+            ( transitive-leq-ℚ r zero-ℚ (rational-abs-ℚ p)
+              ( leq-zero-rational-ℚ⁰⁺ (abs-ℚ p))
+              ( r≤0))
+            ( transitive-leq-ℚ (neg-ℚ r) (neg-ℚ p) (rational-abs-ℚ p)
+              ( neg-leq-abs-ℚ p)
+              ( neg-leq-ℚ _ _ p≤r))))
+      ( λ 0≤r →
+        transitive-leq-ℚ
+          ( rational-abs-ℚ r)
+          ( rational-abs-ℚ q)
+          ( max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+          ( leq-right-max-ℚ _ _)
+          ( binary-tr
+            ( leq-ℚ)
+            ( inv (rational-abs-zero-leq-ℚ r 0≤r))
+            ( inv
+              ( rational-abs-zero-leq-ℚ
+                ( q)
+                ( transitive-leq-ℚ zero-ℚ r q r≤q 0≤r)))
+            ( r≤q)))
+      ( linear-leq-ℚ r zero-ℚ)
+```
diff --git a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md
index bb3cf3e048..93b5e7586e 100644
--- a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md
@@ -11,12 +11,14 @@ module elementary-number-theory.absolute-value-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-nonnegative-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-nonnegative-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.multiplication-nonnegative-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -127,6 +129,16 @@ opaque
         ( q≤0))
 ```
 
+### The absolute value of a positive rational number is the number itself
+
+```agda
+abstract
+  rational-abs-rational-ℚ⁺ :
+    (q : ℚ⁺) → rational-abs-ℚ (rational-ℚ⁺ q) ＝ rational-ℚ⁺ q
+  rational-abs-rational-ℚ⁺ q =
+    ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (nonnegative-ℚ⁺ q))
+```
+
 ### The absolute value of the negation of `q` is the absolute value of `q`
 
 ```agda
@@ -211,6 +223,14 @@ abstract
           { rational-abs-ℚ q}
           ( neg-leq-abs-ℚ p)
           ( neg-leq-abs-ℚ q)))
+
+  triangle-inequality-abs-diff-ℚ :
+    (p q : ℚ) → leq-ℚ⁰⁺ (abs-ℚ (p -ℚ q)) (abs-ℚ p +ℚ⁰⁺ abs-ℚ q)
+  triangle-inequality-abs-diff-ℚ p q =
+    tr
+      ( leq-ℚ⁰⁺ (abs-ℚ (p -ℚ q)))
+      ( ap-binary add-ℚ⁰⁺ (refl {x = abs-ℚ p}) (abs-neg-ℚ q))
+      ( triangle-inequality-abs-ℚ p (neg-ℚ q))
 ```
 
 ### `|ab| = |a||b|`
@@ -288,4 +308,9 @@ opaque
                   is-nonnegative-leq-zero-ℚ (neg-ℚ p) (neg-leq-ℚ p zero-ℚ p≤0)))
         ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
           by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-leq-zero-ℚ p p≤0)))
+
+abstract
+  rational-abs-mul-ℚ :
+    (p q : ℚ) → rational-abs-ℚ (p *ℚ q) ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
+  rational-abs-mul-ℚ p q = ap rational-ℚ⁰⁺ (abs-mul-ℚ p q)
 ```
diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md
index a36bedf713..8d887c25a6 100644
--- a/src/elementary-number-theory/addition-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md
@@ -11,6 +11,7 @@ module elementary-number-theory.addition-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-integers
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.natural-numbers
@@ -33,9 +34,9 @@ open import foundation.sections
 ## Idea
 
 We introduce
-{{#concept "addition" WDID=Q32043 WD="addition" Disambiguation="rational numbers" Agda=add-ℚ}}
-on the [rational numbers](elementary-number-theory.rational-numbers.md) and
-derive its basic properties.
+{{#concept "addition" Disambiguation="rational numbers" Agda=add-ℚ}} on the
+[rational numbers](elementary-number-theory.rational-numbers.md) and derive its
+basic properties.
 
 ## Definition
 
@@ -304,6 +305,15 @@ abstract
       by is-retraction-rational-fraction-ℚ (rational-ℤ (x +ℤ y))
 ```
 
+### The inclusion of natural numbers preserves addition
+
+```agda
+add-rational-ℕ :
+  (m n : ℕ) → rational-ℕ m +ℚ rational-ℕ n ＝ rational-ℕ (m +ℕ n)
+add-rational-ℕ m n =
+  add-rational-ℤ _ _ ∙ ap rational-ℤ (add-int-ℕ m n)
+```
+
 ### The rational successor of an integer is the successor of the integer
 
 ```agda
diff --git a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md
index dc4fd7b441..59ab924007 100644
--- a/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md
@@ -25,6 +25,9 @@ open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
 open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
+
+open import logic.functoriality-existential-quantification
 ```
 
 </details>
@@ -75,3 +78,17 @@ abstract
   archimedean-property-ℚ x y pos-x =
     unit-trunc-Prop (bound-archimedean-property-ℚ x y pos-x)
 ```
+
+## Corollaries
+
+### For any rational `q`, there exists a natural number `n` with `q < n`
+
+```agda
+abstract
+  exists-greater-natural-ℚ :
+    (q : ℚ) → exists ℕ (λ n → le-ℚ-Prop q (rational-ℕ n))
+  exists-greater-natural-ℚ q =
+    map-tot-exists
+      ( λ _ → tr (le-ℚ q) (right-unit-law-mul-ℚ _))
+      ( archimedean-property-ℚ one-ℚ q _)
+```
diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md
index 1dfb7131df..d2f510c051 100644
--- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md
@@ -8,6 +8,7 @@ module elementary-number-theory.closed-intervals-rational-numbers where
 
 ```agda
 open import elementary-number-theory.decidable-total-order-rational-numbers
+open import elementary-number-theory.distance-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.minimum-rational-numbers
@@ -83,9 +84,17 @@ is-below-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-below-prop-closed-interval-ℚ ((a , _) , _) b = le-ℚ-Prop b a
 
+is-below-closed-interval-ℚ : closed-interval-ℚ → ℚ → UU lzero
+is-below-closed-interval-ℚ [a,b] q =
+  type-Prop (is-below-prop-closed-interval-ℚ [a,b] q)
+
 is-above-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-above-prop-closed-interval-ℚ ((_ , a) , _) b = le-ℚ-Prop a b
+
+is-above-closed-interval-ℚ : closed-interval-ℚ → ℚ → UU lzero
+is-above-closed-interval-ℚ [a,b] q =
+  type-Prop (is-above-prop-closed-interval-ℚ [a,b] q)
 ```
 
 ### The width of a closed interval
@@ -177,3 +186,26 @@ upper-bound-is-in-closed-interval-ℚ :
 upper-bound-is-in-closed-interval-ℚ =
   upper-bound-is-in-closed-interval-Poset ℚ-Poset
 ```
+
+### The distance between the lower and upper bounds of a closed interval is its width
+
+```agda
+abstract
+  eq-width-dist-lower-upper-bounds-closed-interval-ℚ :
+    ([a,b] : closed-interval-ℚ) →
+    rational-dist-ℚ
+      ( lower-bound-closed-interval-ℚ [a,b])
+      ( upper-bound-closed-interval-ℚ [a,b]) ＝
+    width-closed-interval-ℚ [a,b]
+  eq-width-dist-lower-upper-bounds-closed-interval-ℚ ((a , b) , a≤b) =
+    eq-dist-diff-leq-ℚ a b a≤b
+
+  eq-width-dist-upper-lower-bounds-closed-interval-ℚ :
+    ([a,b] : closed-interval-ℚ) →
+    rational-dist-ℚ
+      ( upper-bound-closed-interval-ℚ [a,b])
+      ( lower-bound-closed-interval-ℚ [a,b]) ＝
+    width-closed-interval-ℚ [a,b]
+  eq-width-dist-upper-lower-bounds-closed-interval-ℚ ((a , b) , a≤b) =
+    eq-dist-diff-leq-ℚ' b a a≤b
+```
diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md
index 8d41ac3325..8576576ca6 100644
--- a/src/elementary-number-theory/distance-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/distance-rational-numbers.lagda.md
@@ -64,6 +64,18 @@ abstract
     inv (abs-neg-ℚ _) ∙ ap abs-ℚ (distributive-neg-diff-ℚ _ _)
 ```
 
+### A rational number's distance from itself is zero
+
+```agda
+abstract
+  dist-self-ℚ : (q : ℚ) → dist-ℚ q q ＝ zero-ℚ⁰⁺
+  dist-self-ℚ q =
+    ap abs-ℚ (right-inverse-law-add-ℚ q) ∙ abs-rational-ℚ⁰⁺ zero-ℚ⁰⁺
+
+  rational-dist-self-ℚ : (q : ℚ) → rational-dist-ℚ q q ＝ zero-ℚ
+  rational-dist-self-ℚ q = ap rational-ℚ⁰⁺ (dist-self-ℚ q)
+```
+
 ### The differences of the arguments are less than or equal to their distance
 
 ```agda
@@ -225,6 +237,11 @@ abstract
             ( q -ℚ p)
             ( backward-implication (iff-translate-diff-leq-zero-ℚ p q) p≤q)
 
+  eq-dist-diff-leq-ℚ' : (p q : ℚ) → leq-ℚ q p → rational-dist-ℚ p q ＝ p -ℚ q
+  eq-dist-diff-leq-ℚ' p q q≤p =
+    ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _) ∙
+    eq-dist-diff-leq-ℚ q p q≤p
+
   eq-dist-diff-max-min-ℚ :
     (p q : ℚ) → rational-dist-ℚ p q ＝ max-ℚ p q -ℚ min-ℚ p q
   eq-dist-diff-max-min-ℚ p q =
diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
index ebb650550e..5ebe72f523 100644
--- a/src/elementary-number-theory/inequality-integers.lagda.md
+++ b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -215,20 +215,37 @@ reflects-leq-right-add-ℤ z x y =
   is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z)
 ```
 
-### The inclusion of ℕ into ℤ preserves inequality
+### The inclusion of ℕ into ℤ preserves and reflects inequality
 
 ```agda
-leq-int-ℕ : (x y : ℕ) → leq-ℕ x y → leq-ℤ (int-ℕ x) (int-ℕ y)
-leq-int-ℕ zero-ℕ y H =
-  tr
-    ( is-nonnegative-ℤ)
-    ( inv (right-unit-law-add-ℤ (int-ℕ y)))
-    ( is-nonnegative-int-ℕ y)
-leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H = tr (is-nonnegative-ℤ)
-  ( inv (diff-succ-ℤ (int-ℕ y) (int-ℕ x)) ∙
-    ( ap (_-ℤ (succ-ℤ (int-ℕ x))) (succ-int-ℕ y) ∙
-      ap ((int-ℕ (succ-ℕ y)) -ℤ_) (succ-int-ℕ x)))
-  ( leq-int-ℕ x y H)
+abstract
+  leq-int-ℕ : (x y : ℕ) → leq-ℕ x y → leq-ℤ (int-ℕ x) (int-ℕ y)
+  leq-int-ℕ zero-ℕ y H =
+    tr
+      ( is-nonnegative-ℤ)
+      ( inv (right-unit-law-add-ℤ (int-ℕ y)))
+      ( is-nonnegative-int-ℕ y)
+  leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H =
+    tr
+      ( is-nonnegative-ℤ)
+      ( ( inv (diff-succ-ℤ (int-ℕ y) (int-ℕ x))) ∙
+        ( ap (_-ℤ (succ-ℤ (int-ℕ x))) (succ-int-ℕ y)) ∙
+        ( ap ((int-ℕ (succ-ℕ y)) -ℤ_) (succ-int-ℕ x)))
+      ( leq-int-ℕ x y H)
+
+  reflects-leq-int-ℕ : (x y : ℕ) → leq-ℤ (int-ℕ x) (int-ℕ y) → leq-ℕ x y
+  reflects-leq-int-ℕ zero-ℕ y x≤y = star
+  reflects-leq-int-ℕ (succ-ℕ x) (succ-ℕ y) x≤y =
+    reflects-leq-int-ℕ x y
+      ( tr
+        ( is-nonnegative-ℤ)
+        ( ap-diff-ℤ (inv (succ-int-ℕ y)) (inv (succ-int-ℕ x)) ∙
+          diff-succ-ℤ (int-ℕ y) (int-ℕ x))
+        ( x≤y))
+
+  iff-leq-int-ℕ : (x y : ℕ) → leq-ℕ x y ↔ leq-ℤ (int-ℕ x) (int-ℕ y)
+  pr1 (iff-leq-int-ℕ x y) = leq-int-ℕ x y
+  pr2 (iff-leq-int-ℕ x y) = reflects-leq-int-ℕ x y
 ```
 
 ### An integer `x` is nonnegative if and only if `0 ≤ x`
diff --git a/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md
index e6497b8261..7ec428e6cf 100644
--- a/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md
@@ -7,12 +7,15 @@ module elementary-number-theory.inequality-nonnegative-rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.decidable-total-order-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.nonnegative-rational-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.universe-levels
+
+open import order-theory.decidable-total-orders
 ```
 
 </details>
@@ -36,3 +39,15 @@ leq-prop-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ-Prop p q
 leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero
 leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q
 ```
+
+## Properties
+
+### The decidable total order of nonnegative rational numbers
+
+```agda
+decidable-total-order-ℚ⁰⁺ : Decidable-Total-Order lzero lzero
+decidable-total-order-ℚ⁰⁺ =
+  decidable-total-order-Decidable-Total-Suborder
+    ℚ-Decidable-Total-Order
+    is-nonnegative-prop-ℚ
+```
diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
index 91c19d01ae..39552d3082 100644
--- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
@@ -17,9 +17,11 @@ open import elementary-number-theory.difference-integers
 open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-integer-fractions
 open import elementary-number-theory.inequality-integers
+open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonnegative-integers
 open import elementary-number-theory.nonpositive-integers
 open import elementary-number-theory.positive-and-negative-integers
@@ -28,6 +30,7 @@ open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.reduced-integer-fractions
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.cartesian-product-types
 open import foundation.conjunction
 open import foundation.coproduct-types
@@ -284,6 +287,51 @@ module _
   pr2 iff-leq-left-rational-fraction-ℤ = reflects-leq-left-rational-fraction-ℤ
 ```
 
+### The canonical map from integers to the rational numbers preserves and reflects inequality
+
+```agda
+opaque
+  unfolding leq-ℚ-Prop
+
+  preserves-leq-rational-ℤ :
+    (x y : ℤ) → leq-ℤ x y → leq-ℚ (rational-ℤ x) (rational-ℤ y)
+  preserves-leq-rational-ℤ x y =
+    binary-tr leq-ℤ
+      ( inv (right-unit-law-mul-ℤ x))
+      ( inv (right-unit-law-mul-ℤ y))
+
+  reflects-leq-rational-ℤ :
+    (x y : ℤ) → leq-ℚ (rational-ℤ x) (rational-ℤ y) → leq-ℤ x y
+  reflects-leq-rational-ℤ x y =
+    binary-tr leq-ℤ
+      ( right-unit-law-mul-ℤ x)
+      ( right-unit-law-mul-ℤ y)
+
+  iff-leq-rational-ℤ :
+    (x y : ℤ) → leq-ℤ x y ↔ leq-ℚ (rational-ℤ x) (rational-ℤ y)
+  pr1 (iff-leq-rational-ℤ x y) = preserves-leq-rational-ℤ x y
+  pr2 (iff-leq-rational-ℤ x y) = reflects-leq-rational-ℤ x y
+```
+
+### The canonical map from natural numbers to the rational numbers preserves and reflects inequality
+
+```agda
+abstract
+  iff-leq-rational-ℕ :
+    (x y : ℕ) → leq-ℕ x y ↔ leq-ℚ (rational-ℕ x) (rational-ℕ y)
+  iff-leq-rational-ℕ x y =
+    iff-leq-rational-ℤ (int-ℕ x) (int-ℕ y) ∘iff
+    iff-leq-int-ℕ x y
+
+  preserves-leq-rational-ℕ :
+    (x y : ℕ) → leq-ℕ x y → leq-ℚ (rational-ℕ x) (rational-ℕ y)
+  preserves-leq-rational-ℕ x y = forward-implication (iff-leq-rational-ℕ x y)
+
+  reflects-leq-rational-ℕ :
+    (x y : ℕ) → leq-ℚ (rational-ℕ x) (rational-ℕ y) → leq-ℕ x y
+  reflects-leq-rational-ℕ x y = backward-implication (iff-leq-rational-ℕ x y)
+```
+
 ### `x ≤ y` if and only if `0 ≤ y - x`
 
 ```agda
diff --git a/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md
new file mode 100644
index 0000000000..1bd6c1e4d2
--- /dev/null
+++ b/src/elementary-number-theory/maximum-nonnegative-rational-numbers.lagda.md
@@ -0,0 +1,87 @@
+# The maximum of nonnegative rational numbers
+
+```agda
+module elementary-number-theory.maximum-nonnegative-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-nonnegative-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "maximum" Disambiguation="of two nonnegative rational numbers" Agda=max-ℚ⁰⁺}}
+of two
+[nonnegative rational numbers](elementary-number-theory.nonnegative-rational-numbers.md)
+is the
+[greatest](elementary-number-theory.inequality-nonnegative-rational-numbers.md)
+rational number of the two.
+
+## Definition
+
+```agda
+abstract
+  is-nonnegative-max-ℚ⁰⁺ :
+    (p q : ℚ⁰⁺) → is-nonnegative-ℚ (max-ℚ (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q))
+  is-nonnegative-max-ℚ⁰⁺ (p , is-nonneg-p) (q , is-nonneg-q) =
+    is-nonnegative-leq-zero-ℚ _
+      ( transitive-leq-ℚ
+        ( zero-ℚ)
+        ( p)
+        ( max-ℚ p q)
+        ( leq-left-max-ℚ p q)
+        ( leq-zero-is-nonnegative-ℚ p is-nonneg-p))
+
+max-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
+max-ℚ⁰⁺ p⁰⁺@(p , _) q⁰⁺@(q , _) = (max-ℚ p q , is-nonnegative-max-ℚ⁰⁺ p⁰⁺ q⁰⁺)
+```
+
+## Properties
+
+### The binary maximum is associative
+
+```agda
+abstract
+  associative-max-ℚ⁰⁺ :
+    (x y z : ℚ⁰⁺) → max-ℚ⁰⁺ (max-ℚ⁰⁺ x y) z ＝ max-ℚ⁰⁺ x (max-ℚ⁰⁺ y z)
+  associative-max-ℚ⁰⁺ (x , _) (y , _) (z , _) = eq-ℚ⁰⁺ (associative-max-ℚ x y z)
+```
+
+### The binary maximum is commutative
+
+```agda
+abstract
+  commutative-max-ℚ⁰⁺ : (x y : ℚ⁰⁺) → max-ℚ⁰⁺ x y ＝ max-ℚ⁰⁺ y x
+  commutative-max-ℚ⁰⁺ (x , _) (y , _) = eq-ℚ⁰⁺ (commutative-max-ℚ x y)
+```
+
+### The binary maximum is idempotent
+
+```agda
+abstract
+  idempotent-max-ℚ⁰⁺ : (x : ℚ⁰⁺) → max-ℚ⁰⁺ x x ＝ x
+  idempotent-max-ℚ⁰⁺ (x , _) = eq-ℚ⁰⁺ (idempotent-max-ℚ x)
+```
+
+### The binary maximum is an upper bound
+
+```agda
+abstract
+  leq-left-max-ℚ⁰⁺ : (x y : ℚ⁰⁺) → leq-ℚ⁰⁺ x (max-ℚ⁰⁺ x y)
+  leq-left-max-ℚ⁰⁺ _ _ = leq-left-max-ℚ _ _
+
+  leq-right-max-ℚ⁰⁺ : (x y : ℚ⁰⁺) → leq-ℚ⁰⁺ y (max-ℚ⁰⁺ x y)
+  leq-right-max-ℚ⁰⁺ _ _ = leq-right-max-ℚ _ _
+```
diff --git a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
index 0dac1bcf1e..761616c9dc 100644
--- a/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md
@@ -7,16 +7,23 @@ module elementary-number-theory.multiplication-closed-intervals-rational-numbers
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.absolute-value-closed-intervals-rational-numbers
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.addition-closed-intervals-rational-numbers
+open import elementary-number-theory.addition-nonnegative-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.additive-group-of-rational-numbers
 open import elementary-number-theory.closed-interval-preserving-maps-rational-numbers
 open import elementary-number-theory.closed-intervals-rational-numbers
 open import elementary-number-theory.decidable-total-order-rational-numbers
 open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.distance-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-nonnegative-rational-numbers
 open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.minima-and-maxima-rational-numbers
 open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.multiplication-nonnegative-rational-numbers
 open import elementary-number-theory.multiplication-positive-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
@@ -24,6 +31,7 @@ open import elementary-number-theory.multiplicative-group-of-rational-numbers
 open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
 open import elementary-number-theory.negation-closed-intervals-rational-numbers
 open import elementary-number-theory.negative-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
 open import elementary-number-theory.poset-closed-intervals-rational-numbers
 open import elementary-number-theory.positive-and-negative-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
@@ -31,6 +39,7 @@ open import elementary-number-theory.proper-closed-intervals-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
+open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
 open import foundation.cartesian-product-types
@@ -50,12 +59,14 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.groups
 open import group-theory.minkowski-multiplication-commutative-monoids
 open import group-theory.monoids
 open import group-theory.semigroups
 
 open import order-theory.closed-intervals-total-orders
 open import order-theory.decidable-total-orders
+open import order-theory.posets
 open import order-theory.total-orders
 ```
 
@@ -864,3 +875,374 @@ abstract
             ( neg-closed-interval-ℚ)
             ( commutative-mul-closed-interval-ℚ [c,d] [a,b])
 ```
+
+### Bounds on the width of the product of intervals
+
+We can bound the width of the interval $[a,b] ∙ [c,d]$:
+
+$$
+\max(a · c, a · d, b · c, b · d) - \min(a · c, a · d, b · c, b · d) ≤
+  (b - a) ·
+  \max(\left\lvert c\right\rvert , \left\lvert d\right\rvert ) +
+  (d - c) · \max(\left\lvert a\right\rvert , \left\lvert b\right\rvert )
+$$
+
+```agda
+abstract
+  bound-width-mul-closed-interval-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) →
+    leq-ℚ
+      ( width-closed-interval-ℚ (mul-closed-interval-ℚ [a,b] [c,d]))
+      ( ( width-closed-interval-ℚ [a,b] *ℚ
+          rational-max-abs-closed-interval-ℚ [c,d]) +ℚ
+        ( width-closed-interval-ℚ [c,d] *ℚ
+          rational-max-abs-closed-interval-ℚ [a,b]))
+  bound-width-mul-closed-interval-ℚ
+    [a,b]@((a , b) , a≤b) [c,d]@((c , d) , c≤d) =
+    let
+      open inequality-reasoning-Poset ℚ-Poset
+      <b-a><max|c||d|>⁰⁺ =
+        mul-ℚ⁰⁺
+          ( nonnegative-diff-leq-ℚ a b a≤b)
+          ( max-ℚ⁰⁺ (abs-ℚ c) (abs-ℚ d))
+      <b-a><max|c||d|> = rational-ℚ⁰⁺ <b-a><max|c||d|>⁰⁺
+      <d-c><max|a||b|>⁰⁺ =
+        mul-ℚ⁰⁺
+          ( nonnegative-diff-leq-ℚ c d c≤d)
+          ( max-ℚ⁰⁺ (abs-ℚ a) (abs-ℚ b))
+      <d-c><max|a||b|> = rational-ℚ⁰⁺ <d-c><max|a||b|>⁰⁺
+      under-bound : ℚ → UU lzero
+      under-bound q = leq-ℚ q (<b-a><max|c||d|> +ℚ <d-c><max|a||b|>)
+      |aq-bq|≤<b-a>max|c||d| :
+        (q : ℚ) → is-in-closed-interval-ℚ [c,d] q →
+        leq-ℚ (rational-dist-ℚ (a *ℚ q) (b *ℚ q)) <b-a><max|c||d|>
+      |aq-bq|≤<b-a>max|c||d| q q∈[c,d] =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ q) (b *ℚ q)
+          ≤ rational-dist-ℚ a b *ℚ rational-abs-ℚ q
+            by
+              leq-eq-ℚ _ _
+                ( ( ap
+                    ( rational-abs-ℚ)
+                    ( inv (right-distributive-mul-diff-ℚ _ _ _))) ∙
+                  ( rational-abs-mul-ℚ _ _))
+          ≤ rational-dist-ℚ a b *ℚ rational-max-abs-closed-interval-ℚ [c,d]
+            by
+              preserves-leq-left-mul-ℚ⁰⁺
+                ( dist-ℚ a b)
+                ( _)
+                ( _)
+                ( leq-max-abs-is-in-closed-interval-ℚ [c,d] q q∈[c,d])
+          ≤ width-closed-interval-ℚ [a,b] *ℚ
+            rational-max-abs-closed-interval-ℚ [c,d]
+            by
+              leq-eq-ℚ _ _
+                ( ap-mul-ℚ
+                  ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [a,b])
+                  ( refl))
+      |pc-pd|≤<d-c>max|a||b| :
+        (p : ℚ) → is-in-closed-interval-ℚ [a,b] p →
+        leq-ℚ (rational-dist-ℚ (p *ℚ c) (p *ℚ d)) <d-c><max|a||b|>
+      |pc-pd|≤<d-c>max|a||b| p p∈[a,b] =
+        chain-of-inequalities
+          rational-dist-ℚ (p *ℚ c) (p *ℚ d)
+          ≤ rational-dist-ℚ c d *ℚ rational-abs-ℚ p
+            by
+              leq-eq-ℚ _ _
+                ( ( ap
+                    ( rational-abs-ℚ)
+                    ( inv (left-distributive-mul-diff-ℚ _ _ _))) ∙
+                  ( rational-abs-mul-ℚ _ _) ∙
+                  ( commutative-mul-ℚ _ _))
+          ≤ rational-dist-ℚ c d *ℚ rational-max-abs-closed-interval-ℚ [a,b]
+            by
+              preserves-leq-left-mul-ℚ⁰⁺
+                ( dist-ℚ c d)
+                ( _)
+                ( _)
+                ( leq-max-abs-is-in-closed-interval-ℚ [a,b] p p∈[a,b])
+          ≤ _
+            by
+              leq-eq-ℚ _ _
+                ( ap-mul-ℚ
+                  ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [c,d])
+                  ( refl))
+      |ac-bc|≤<b-a>max|c||d| =
+        |aq-bq|≤<b-a>max|c||d| c (lower-bound-is-in-closed-interval-ℚ [c,d])
+      |ad-bd|≤<b-a>max|c||d| =
+        |aq-bq|≤<b-a>max|c||d| d (upper-bound-is-in-closed-interval-ℚ [c,d])
+      |ac-ad|≤<d-c>max|a||b| =
+        |pc-pd|≤<d-c>max|a||b| a (lower-bound-is-in-closed-interval-ℚ [a,b])
+      |bc-bd|≤<d-c>max|a||b| =
+        |pc-pd|≤<d-c>max|a||b| b (upper-bound-is-in-closed-interval-ℚ [a,b])
+      under-bound-|ac-bd| =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ c) (b *ℚ d)
+          ≤ rational-abs-ℚ ((a *ℚ c -ℚ b *ℚ c) +ℚ (b *ℚ c -ℚ b *ℚ d))
+            by
+              leq-eq-ℚ _ _
+                ( ap
+                  ( rational-abs-ℚ)
+                  ( inv ( mul-right-div-Group group-add-ℚ _ _ _)))
+          ≤ _ +ℚ _
+            by triangle-inequality-abs-ℚ _ _
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by preserves-leq-add-ℚ |ac-bc|≤<b-a>max|c||d| |bc-bd|≤<d-c>max|a||b|
+      under-bound-|ad-bc| =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ d) (b *ℚ c)
+          ≤ rational-abs-ℚ ((a *ℚ d -ℚ b *ℚ d) +ℚ (b *ℚ d -ℚ b *ℚ c))
+            by
+              leq-eq-ℚ _ _
+                ( ap
+                  ( rational-abs-ℚ)
+                  ( inv ( mul-right-div-Group group-add-ℚ _ _ _)))
+          ≤ rational-dist-ℚ (a *ℚ d) (b *ℚ d) +ℚ
+            rational-dist-ℚ (b *ℚ d) (b *ℚ c)
+            by triangle-inequality-abs-ℚ _ _
+          ≤ rational-dist-ℚ (a *ℚ d) (b *ℚ d) +ℚ
+            rational-dist-ℚ (b *ℚ c) (b *ℚ d)
+            by
+              leq-eq-ℚ _ _
+                ( ap-add-ℚ refl (ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _)))
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by preserves-leq-add-ℚ |ad-bd|≤<b-a>max|c||d| |bc-bd|≤<d-c>max|a||b|
+      under-bound-|ac-bc| =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ c) (b *ℚ c)
+          ≤ <b-a><max|c||d|>
+            by |ac-bc|≤<b-a>max|c||d|
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by is-inflationary-map-right-add-rational-ℚ⁰⁺ <d-c><max|a||b|>⁰⁺ _
+      under-bound-|ad-bd| =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ d) (b *ℚ d)
+          ≤ <b-a><max|c||d|>
+            by |ad-bd|≤<b-a>max|c||d|
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by is-inflationary-map-right-add-rational-ℚ⁰⁺ <d-c><max|a||b|>⁰⁺ _
+      under-bound-|ac-ad| =
+        chain-of-inequalities
+          rational-dist-ℚ (a *ℚ c) (a *ℚ d)
+          ≤ <d-c><max|a||b|>
+            by |ac-ad|≤<d-c>max|a||b|
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by is-inflationary-map-left-add-rational-ℚ⁰⁺ <b-a><max|c||d|>⁰⁺ _
+      under-bound-|bc-bd| =
+        chain-of-inequalities
+          rational-dist-ℚ (b *ℚ c) (b *ℚ d)
+          ≤ <d-c><max|a||b|>
+            by |bc-bd|≤<d-c>max|a||b|
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by is-inflationary-map-left-add-rational-ℚ⁰⁺ <b-a><max|c||d|>⁰⁺ _
+      under-bound-|q-q| q =
+        chain-of-inequalities
+          rational-dist-ℚ q q
+          ≤ zero-ℚ
+            by leq-eq-ℚ _ _ (rational-dist-self-ℚ q)
+          ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
+            by
+              leq-zero-rational-ℚ⁰⁺ (<b-a><max|c||d|>⁰⁺ +ℚ⁰⁺ <d-c><max|a||b|>⁰⁺)
+      [a,b][c,d]@((min , max) , _) = mul-closed-interval-ℚ [a,b] [c,d]
+      case-1 :
+        {p q : ℚ} → (min ＝ p) → under-bound (rational-dist-ℚ p q) →
+        (max ＝ q) → under-bound (width-closed-interval-ℚ [a,b][c,d])
+      case-1 min=p bound-|p-q| max=q =
+        tr
+          ( under-bound)
+          ( ap-binary rational-dist-ℚ (inv min=p) (inv max=q) ∙
+            eq-width-dist-lower-upper-bounds-closed-interval-ℚ [a,b][c,d])
+          ( bound-|p-q|)
+      case-2 :
+        {p q : ℚ} → (min ＝ p) → under-bound (rational-dist-ℚ q p) →
+        (max ＝ q) → under-bound (width-closed-interval-ℚ [a,b][c,d])
+      case-2 min=p bound-|q-p| =
+        case-1
+          ( min=p)
+          ( tr
+            ( under-bound)
+            ( ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _))
+            ( bound-|q-p|))
+      case-eq :
+        {p : ℚ} → (min ＝ p) → (max ＝ p) →
+        under-bound (width-closed-interval-ℚ [a,b][c,d])
+      case-eq min=p = case-1 min=p (under-bound-|q-q| _)
+      motive =
+        leq-ℚ-Prop
+          ( width-closed-interval-ℚ [a,b][c,d])
+          ( <b-a><max|c||d|> +ℚ <d-c><max|a||b|>)
+      case-max =
+        eq-one-of-four-max-Total-Order
+          ( ℚ-Total-Order)
+          ( motive)
+          ( a *ℚ c)
+          ( a *ℚ d)
+          ( b *ℚ c)
+          ( b *ℚ d)
+    in
+      eq-one-of-four-min-Total-Order
+        ( ℚ-Total-Order)
+        ( motive)
+        ( a *ℚ c)
+        ( a *ℚ d)
+        ( b *ℚ c)
+        ( b *ℚ d)
+        ( λ min=ac →
+          case-max
+            ( case-eq min=ac)
+            ( case-1 min=ac under-bound-|ac-ad|)
+            ( case-1 min=ac under-bound-|ac-bc|)
+            ( case-1 min=ac under-bound-|ac-bd|))
+        ( λ min=ad →
+          case-max
+            ( case-2 min=ad under-bound-|ac-ad|)
+            ( case-eq min=ad)
+            ( case-1 min=ad under-bound-|ad-bc|)
+            ( case-1 min=ad under-bound-|ad-bd|))
+        ( λ min=bc →
+          case-max
+            ( case-2 min=bc under-bound-|ac-bc|)
+            ( case-2 min=bc under-bound-|ad-bc|)
+            ( case-eq min=bc)
+            ( case-1 min=bc under-bound-|bc-bd|))
+        ( λ min=bd →
+          case-max
+            ( case-2 min=bd under-bound-|ac-bd|)
+            ( case-2 min=bd under-bound-|ad-bd|)
+            ( case-2 min=bd under-bound-|bc-bd|)
+            ( case-eq min=bd))
+```
+
+### Multiplication of closed intervals is subdistributive
+
+```agda
+abstract
+  left-subdistributive-mul-add-closed-interval-ℚ :
+    ([a,b] [c,d] [e,f] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] (add-closed-interval-ℚ [c,d] [e,f]))
+      ( add-closed-interval-ℚ
+        ( mul-closed-interval-ℚ [a,b] [c,d])
+        ( mul-closed-interval-ℚ [a,b] [e,f]))
+  left-subdistributive-mul-add-closed-interval-ℚ [a,b] [c,d] [e,f] =
+    leq-closed-interval-leq-subtype-ℚ
+      ( mul-closed-interval-ℚ [a,b] (add-closed-interval-ℚ [c,d] [e,f]))
+      ( add-closed-interval-ℚ
+        ( mul-closed-interval-ℚ [a,b] [c,d])
+        ( mul-closed-interval-ℚ [a,b] [e,f]))
+      ( λ q q∈[a,b]⟨[c,d]+[e,f]⟩ →
+        let
+          open
+            do-syntax-trunc-Prop
+              ( subtype-closed-interval-ℚ
+                ( add-closed-interval-ℚ
+                  ( mul-closed-interval-ℚ [a,b] [c,d])
+                  ( mul-closed-interval-ℚ [a,b] [e,f]))
+                ( q))
+        in do
+          ((qab , qcdef) , qab∈[a,b] , qcdef∈[c,d]+[e,f] , q=qab*qcdef) ←
+            is-in-minkowski-product-is-in-mul-closed-interval-ℚ
+              ( [a,b])
+              ( add-closed-interval-ℚ [c,d] [e,f])
+              ( q)
+              ( q∈[a,b]⟨[c,d]+[e,f]⟩)
+          ((qcd , qef) , qcd∈[c,d] , qef∈[e,f] , qcdef=qcd+qef) ←
+            is-in-minkowski-sum-is-in-add-closed-interval-ℚ
+              ( [c,d])
+              ( [e,f])
+              ( qcdef)
+              ( qcdef∈[c,d]+[e,f])
+          inv-tr
+            ( is-in-closed-interval-ℚ
+              ( add-closed-interval-ℚ
+                ( mul-closed-interval-ℚ [a,b] [c,d])
+                ( mul-closed-interval-ℚ [a,b] [e,f])))
+            ( ( q=qab*qcdef) ∙
+              ( ap-mul-ℚ refl qcdef=qcd+qef) ∙
+              ( left-distributive-mul-add-ℚ qab qcd qef))
+            ( is-in-add-interval-add-is-in-closed-interval-ℚ
+              ( mul-closed-interval-ℚ [a,b] [c,d])
+              ( mul-closed-interval-ℚ [a,b] [e,f])
+              ( qab *ℚ qcd)
+              ( qab *ℚ qef)
+              ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                  ( [a,b])
+                  ( [c,d])
+                  ( qab)
+                  ( qcd)
+                  ( qab∈[a,b])
+                  ( qcd∈[c,d]))
+              ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                  ( [a,b])
+                  ( [e,f])
+                  ( qab)
+                  ( qef)
+                  ( qab∈[a,b])
+                  ( qef∈[e,f]))))
+```
+
+### Containment of intervals is preserved by multiplication
+
+```agda
+abstract
+  preserves-leq-left-mul-closed-interval-ℚ :
+    ([c,d] [a,b] [a',b'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c,d])
+  preserves-leq-left-mul-closed-interval-ℚ [c,d] [a,b] [a',b'] [a,b]⊆[a',b'] =
+    leq-closed-interval-leq-subtype-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c,d])
+      ( binary-tr
+        ( _⊆_)
+        ( eq-minkowski-mul-closed-interval-ℚ [a,b] [c,d])
+        ( eq-minkowski-mul-closed-interval-ℚ [a',b'] [c,d])
+        ( preserves-leq-left-minkowski-mul-Commutative-Monoid
+          ( commutative-monoid-mul-ℚ)
+          ( subtype-closed-interval-ℚ [c,d])
+          ( subtype-closed-interval-ℚ [a,b])
+          ( subtype-closed-interval-ℚ [a',b'])
+          ( leq-subtype-leq-closed-interval-ℚ [a,b] [a',b'] [a,b]⊆[a',b'])))
+
+  preserves-leq-right-mul-closed-interval-ℚ :
+    ([a,b] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a,b] [c',d'])
+  preserves-leq-right-mul-closed-interval-ℚ [a,b] [c,d] [c',d'] [c,d]⊆[c',d'] =
+    binary-tr
+      ( leq-closed-interval-ℚ)
+      ( commutative-mul-closed-interval-ℚ [c,d] [a,b])
+      ( commutative-mul-closed-interval-ℚ [c',d'] [a,b])
+      ( preserves-leq-left-mul-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+
+  preserves-leq-mul-closed-interval-ℚ :
+    ([a,b] [a',b'] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] → leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c',d'])
+  preserves-leq-mul-closed-interval-ℚ
+    [a,b] [a',b'] [c,d] [c',d'] [a,b]⊆[a',b'] [c,d]⊆[c',d'] =
+    transitive-leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a,b] [c',d'])
+      ( mul-closed-interval-ℚ [a',b'] [c',d'])
+      ( preserves-leq-left-mul-closed-interval-ℚ
+        ( [c',d'])
+        ( [a,b])
+        ( [a',b'])
+        ( [a,b]⊆[a',b']))
+      ( preserves-leq-right-mul-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+```
diff --git a/src/elementary-number-theory/multiplication-nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-nonnegative-rational-numbers.lagda.md
index 7c7e070d5f..203f33961f 100644
--- a/src/elementary-number-theory/multiplication-nonnegative-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplication-nonnegative-rational-numbers.lagda.md
@@ -10,6 +10,7 @@ module elementary-number-theory.multiplication-nonnegative-rational-numbers wher
 
 ```agda
 open import elementary-number-theory.inequality-integers
+open import elementary-number-theory.inequality-nonnegative-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.multiplication-integer-fractions
 open import elementary-number-theory.multiplication-integers
@@ -110,4 +111,15 @@ opaque
       ( commutative-mul-ℚ q (rational-ℚ⁰⁺ p))
       ( commutative-mul-ℚ r (rational-ℚ⁰⁺ p))
       ( preserves-leq-right-mul-ℚ⁰⁺ p q r q≤r)
+
+abstract
+  preserves-leq-mul-ℚ⁰⁺ :
+    (p q r s : ℚ⁰⁺) → leq-ℚ⁰⁺ p q → leq-ℚ⁰⁺ r s → leq-ℚ⁰⁺ (p *ℚ⁰⁺ r) (q *ℚ⁰⁺ s)
+  preserves-leq-mul-ℚ⁰⁺ p q r s p≤q r≤s =
+    transitive-leq-ℚ
+      ( rational-ℚ⁰⁺ (p *ℚ⁰⁺ r))
+      ( rational-ℚ⁰⁺ (p *ℚ⁰⁺ s))
+      ( rational-ℚ⁰⁺ (q *ℚ⁰⁺ s))
+      ( preserves-leq-right-mul-ℚ⁰⁺ s _ _ p≤q)
+      ( preserves-leq-left-mul-ℚ⁰⁺ p _ _ r≤s)
 ```
diff --git a/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md
index 70a33b9e29..855ae9e41f 100644
--- a/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/multiplicative-group-of-positive-rational-numbers.lagda.md
@@ -170,3 +170,11 @@ module _
     eq-denominator-inv-numerator-ℚ⁺ =
       ind-Σ eq-denominator-inv-numerator-is-positive-ℚ x
 ```
+
+### Group laws on the positive rational numbers
+
+```agda
+abstract
+  is-section-right-mul-ℚ⁺ : (p q : ℚ⁺) → (q *ℚ⁺ inv-ℚ⁺ p) *ℚ⁺ p ＝ q
+  is-section-right-mul-ℚ⁺ = is-section-right-div-Group group-mul-ℚ⁺
+```
diff --git a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md
index 22352dc405..c7cd39a748 100644
--- a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md
@@ -17,6 +17,7 @@ open import elementary-number-theory.inequality-integers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.nonnegative-integer-fractions
 open import elementary-number-theory.nonnegative-integers
 open import elementary-number-theory.positive-and-negative-integers
@@ -155,6 +156,13 @@ nonnegative-rational-nonnegative-ℤ (x , x-is-neg) =
   ( rational-ℤ x , is-nonnegative-rational-ℤ x x-is-neg)
 ```
 
+### The images of natural numbers in the rationals are nonnegative
+
+```agda
+nonnegative-rational-ℕ : ℕ → ℚ⁰⁺
+nonnegative-rational-ℕ n = (rational-ℕ n , is-nonnegative-int-ℕ n)
+```
+
 ### The rational image of a nonnegative integer fraction is nonnegative
 
 ```agda
@@ -193,6 +201,11 @@ module _
     is-nonnegative-iff-leq-zero-ℚ =
       ( leq-zero-is-nonnegative-ℚ ,
         is-nonnegative-leq-zero-ℚ)
+
+abstract
+  leq-zero-rational-ℚ⁰⁺ : (p : ℚ⁰⁺) → leq-ℚ zero-ℚ (rational-ℚ⁰⁺ p)
+  leq-zero-rational-ℚ⁰⁺ (p , is-nonneg-p) =
+    leq-zero-is-nonnegative-ℚ p is-nonneg-p
 ```
 
 ### The successor of a nonnegative rational number is positive
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index aba3f11975..4736e4b7c7 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -17,6 +17,7 @@ open import real-numbers.cauchy-completeness-dedekind-real-numbers public
 open import real-numbers.dedekind-real-numbers public
 open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
+open import real-numbers.enclosing-closed-rational-intervals-real-numbers public
 open import real-numbers.finitely-enumerable-subsets-real-numbers public
 open import real-numbers.inequality-lower-dedekind-real-numbers public
 open import real-numbers.inequality-real-numbers public
@@ -36,6 +37,7 @@ open import real-numbers.minimum-finite-families-real-numbers public
 open import real-numbers.minimum-inhabited-finitely-enumerable-subsets-real-numbers public
 open import real-numbers.minimum-lower-dedekind-real-numbers public
 open import real-numbers.minimum-upper-dedekind-real-numbers public
+open import real-numbers.multiplication-real-numbers public
 open import real-numbers.negation-lower-upper-dedekind-real-numbers public
 open import real-numbers.negation-real-numbers public
 open import real-numbers.nonnegative-real-numbers public
diff --git a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md
index 2c0bb2c41c..3fbc4ba1e4 100644
--- a/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md
+++ b/src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md
@@ -9,6 +9,8 @@ module real-numbers.arithmetically-located-dedekind-cuts where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.additive-group-of-rational-numbers
@@ -16,10 +18,12 @@ open import elementary-number-theory.archimedean-property-rational-numbers
 open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.integers
+open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-positive-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
 open import foundation.action-on-identifications-functions
@@ -31,6 +35,7 @@ open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
 open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
@@ -41,6 +46,10 @@ open import foundation.universe-levels
 
 open import group-theory.abelian-groups
 
+open import logic.functoriality-existential-quantification
+
+open import order-theory.posets
+
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.lower-dedekind-real-numbers
 open import real-numbers.upper-dedekind-real-numbers
@@ -84,10 +93,74 @@ module _
   is-arithmetically-located-lower-upper-ℝ : UU (l1 ⊔ l2)
   is-arithmetically-located-lower-upper-ℝ =
     type-Prop is-arithmetically-located-prop-lower-upper-ℝ
+
+close-bounds-ℝ : {l : Level} (x : ℝ l) → ℚ⁺ → subtype l (ℚ × ℚ)
+close-bounds-ℝ x =
+  close-bounds-lower-upper-ℝ (lower-real-ℝ x) (upper-real-ℝ x)
+```
+
+### The predicate of being weakly arithmetically located
+
+```agda
+module _
+  {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2)
+  where
+
+  weak-close-bounds-lower-upper-ℝ : ℚ⁺ → subtype (l1 ⊔ l2) (ℚ × ℚ)
+  weak-close-bounds-lower-upper-ℝ ε⁺ (p , q) =
+    leq-ℚ-Prop q (p +ℚ (rational-ℚ⁺ ε⁺)) ∧
+    cut-lower-ℝ x p ∧
+    cut-upper-ℝ y q
+
+  is-weakly-arithmetically-located-prop-lower-upper-ℝ : Prop (l1 ⊔ l2)
+  is-weakly-arithmetically-located-prop-lower-upper-ℝ =
+    Π-Prop ℚ⁺ (λ ε⁺ → ∃ (ℚ × ℚ) (weak-close-bounds-lower-upper-ℝ ε⁺))
+
+  is-weakly-arithmetically-located-lower-upper-ℝ : UU (l1 ⊔ l2)
+  is-weakly-arithmetically-located-lower-upper-ℝ =
+    type-Prop is-weakly-arithmetically-located-prop-lower-upper-ℝ
 ```
 
 ## Properties
 
+### A cut is weakly arithmetically located if and only if it is arithmetically located
+
+```agda
+module _
+  {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2)
+  where
+
+  abstract
+    is-arithmetically-located-is-weakly-arithmetically-located-lower-upper-ℝ :
+      is-weakly-arithmetically-located-lower-upper-ℝ x y →
+      is-arithmetically-located-lower-upper-ℝ x y
+    is-arithmetically-located-is-weakly-arithmetically-located-lower-upper-ℝ
+      W ε =
+      let
+        ε' = mediant-zero-ℚ⁺ ε
+      in
+        map-tot-exists
+          ( λ (p , q) (q≤p+ε' , p<x , y<q) →
+            ( concatenate-leq-le-ℚ
+              ( q)
+              ( p +ℚ rational-ℚ⁺ ε')
+              ( p +ℚ rational-ℚ⁺ ε)
+              ( q≤p+ε')
+              ( preserves-le-right-add-ℚ p _ _ (le-mediant-zero-ℚ⁺ ε)) ,
+              p<x ,
+              y<q))
+          ( W ε')
+
+    is-weakly-arithmetically-located-is-arithmetically-located-lower-upper-ℝ :
+      is-arithmetically-located-lower-upper-ℝ x y →
+      is-weakly-arithmetically-located-lower-upper-ℝ x y
+    is-weakly-arithmetically-located-is-arithmetically-located-lower-upper-ℝ
+      H ε =
+      map-tot-exists
+        ( λ (p , q) (q<p+ε , p<x , y<q) → (leq-le-ℚ q<p+ε , p<x , y<q))
+        ( H ε)
+```
+
 ### Arithmetically located cuts are located
 
 If a pair of lower and upper Dedekind cuts is arithmetically located, it is also
@@ -132,6 +205,15 @@ module _
                   ( q'∈U)))
             ( decide-le-leq-ℚ p p'))
         ( arithmetically-located (positive-diff-le-ℚ p q p<q))
+
+    is-located-is-weakly-arithmetically-located-lower-upper-ℝ :
+      is-weakly-arithmetically-located-lower-upper-ℝ x y →
+      is-located-lower-upper-ℝ x y
+    is-located-is-weakly-arithmetically-located-lower-upper-ℝ =
+      is-located-is-arithmetically-located-lower-upper-ℝ ∘
+      is-arithmetically-located-is-weakly-arithmetically-located-lower-upper-ℝ
+        ( x)
+        ( y)
 ```
 
 ### The cuts of Dedekind real numbers are arithmetically located
@@ -234,6 +316,138 @@ module _
             x<r+2ε')
 ```
 
+### For any real number `x` and any `ε : ℚ⁺`, there exists `n : ℕ` such that if `q < x < q + ε`, then `|q| < n` and `|q +ℚ ε| < n`
+
+```agda
+abstract
+  natural-bound-location-ℝ :
+    {l : Level} → (x : ℝ l) (ε : ℚ⁺) →
+    exists
+      ( ℕ)
+      ( λ n →
+        Π-Prop
+          ( type-subtype (close-bounds-ℝ x ε))
+          ( λ ((q , q') , _) →
+            le-ℚ-Prop
+              ( max-ℚ (rational-abs-ℚ q) (rational-abs-ℚ q'))
+              ( rational-ℕ n)))
+  natural-bound-location-ℝ x ε⁺@(ε , _) =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( ∃
+            ( ℕ)
+            ( λ n →
+              Π-Prop
+                ( type-subtype (close-bounds-ℝ x ε⁺))
+                ( λ ((q , q') , _) →
+                  le-ℚ-Prop
+                    ( max-ℚ (rational-abs-ℚ q) (rational-abs-ℚ q'))
+                    ( rational-ℕ n))))
+      open inequality-reasoning-Poset ℚ-Poset
+    in do
+      (p , p<x) ← is-inhabited-lower-cut-ℝ x
+      (q , x<q) ← is-inhabited-upper-cut-ℝ x
+      (n , max|p||q|<n) ←
+        exists-greater-natural-ℚ (max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+      (m , ε<m) ← exists-greater-natural-ℚ ε
+      intro-exists
+        ( m +ℕ n +ℕ m)
+        ( λ ((a , b) , b<a+ε , a<x , x<b) →
+          let
+            |a|≤m+n =
+              leq-abs-leq-leq-neg-ℚ
+                ( a)
+                ( rational-ℕ (m +ℕ n))
+                ( chain-of-inequalities
+                    a
+                    ≤ q
+                      by leq-lower-upper-cut-ℝ x a q a<x x<q
+                    ≤ rational-abs-ℚ q
+                      by leq-abs-ℚ q
+                    ≤ ε +ℚ rational-abs-ℚ q
+                      by leq-left-add-rational-ℚ⁺ _ ε⁺
+                    ≤ rational-ℕ m +ℚ
+                      max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q)
+                      by
+                        preserves-leq-add-ℚ
+                          ( leq-le-ℚ ε<m)
+                          ( leq-right-max-ℚ _ _)
+                    ≤ rational-ℕ m +ℚ rational-ℕ n
+                      by preserves-leq-right-add-ℚ _ _ _ (leq-le-ℚ max|p||q|<n)
+                    ≤ rational-ℕ (m +ℕ n)
+                      by leq-eq-ℚ _ _ (add-rational-ℕ _ _))
+                ( chain-of-inequalities
+                    neg-ℚ a
+                    ≤ neg-ℚ (b -ℚ ε)
+                      by
+                        neg-leq-ℚ _ _
+                          ( leq-transpose-right-add-ℚ _ _ _ (leq-le-ℚ b<a+ε))
+                    ≤ ε -ℚ b
+                      by leq-eq-ℚ _ _ (distributive-neg-diff-ℚ _ _)
+                    ≤ ε -ℚ p
+                      by
+                        preserves-leq-right-add-ℚ ε
+                          ( neg-ℚ b)
+                          ( neg-ℚ p)
+                          ( neg-leq-ℚ _ _
+                            ( leq-lower-upper-cut-ℝ x p b p<x x<b))
+                    ≤ rational-abs-ℚ (ε -ℚ p)
+                      by leq-abs-ℚ _
+                    ≤ rational-abs-ℚ ε +ℚ rational-abs-ℚ p
+                      by triangle-inequality-abs-diff-ℚ ε p
+                    ≤ ε +ℚ max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q)
+                      by
+                        preserves-leq-add-ℚ
+                          ( leq-eq-ℚ _ _ (rational-abs-rational-ℚ⁺ ε⁺))
+                          ( leq-left-max-ℚ _ _)
+                    ≤ rational-ℕ m +ℚ rational-ℕ n
+                      by
+                        preserves-leq-add-ℚ
+                          ( leq-le-ℚ ε<m)
+                          ( leq-le-ℚ max|p||q|<n)
+                    ≤ rational-ℕ (m +ℕ n)
+                      by leq-eq-ℚ _ _ (add-rational-ℕ _ _))
+            |b|≤|a|+ε =
+              leq-abs-leq-leq-neg-ℚ b (rational-abs-ℚ a +ℚ ε)
+                ( chain-of-inequalities
+                    b
+                    ≤ a +ℚ ε
+                      by leq-le-ℚ b<a+ε
+                    ≤ rational-abs-ℚ (a +ℚ ε)
+                      by leq-abs-ℚ _
+                    ≤ rational-abs-ℚ a +ℚ rational-abs-ℚ ε
+                      by triangle-inequality-abs-ℚ _ _
+                    ≤ rational-abs-ℚ a +ℚ ε
+                      by
+                        leq-eq-ℚ _ _
+                          ( ap-add-ℚ refl (rational-abs-rational-ℚ⁺ ε⁺)))
+                ( chain-of-inequalities
+                    neg-ℚ b
+                    ≤ neg-ℚ a
+                      by neg-leq-ℚ _ _ (leq-lower-upper-cut-ℝ x a b a<x x<b)
+                    ≤ rational-abs-ℚ a
+                      by neg-leq-abs-ℚ a
+                    ≤ rational-abs-ℚ a +ℚ ε
+                      by leq-right-add-rational-ℚ⁺ _ ε⁺)
+          in
+            concatenate-leq-le-ℚ
+              ( max-ℚ (rational-abs-ℚ a) (rational-abs-ℚ b))
+              ( rational-ℕ (m +ℕ n) +ℚ ε)
+              ( rational-ℕ (m +ℕ n +ℕ m))
+              ( leq-max-leq-both-ℚ _ _ _
+                ( transitive-leq-ℚ _ (rational-ℕ (m +ℕ n)) _
+                  ( leq-right-add-rational-ℚ⁺ _ ε⁺)
+                  ( |a|≤m+n))
+                ( transitive-leq-ℚ _ (rational-abs-ℚ a +ℚ ε) _
+                  ( preserves-leq-left-add-ℚ _ _ _ |a|≤m+n)
+                  ( |b|≤|a|+ε)))
+              ( tr
+                ( le-ℚ (rational-ℕ (m +ℕ n) +ℚ ε))
+                ( add-rational-ℕ _ _)
+                ( preserves-le-right-add-ℚ _ _ _ ε<m)))
+```
+
 ## References
 
 {{#bibliography}}
diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md
index 4b693a23ff..83131eeaac 100644
--- a/src/real-numbers/dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/dedekind-real-numbers.lagda.md
@@ -8,6 +8,8 @@ module real-numbers.dedekind-real-numbers where
 
 ```agda
 open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -28,6 +30,7 @@ open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
+open import foundation.inhabited-types
 open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.powersets
@@ -253,18 +256,25 @@ module _
   {l : Level} (x : ℝ l) (p q : ℚ)
   where
 
-  le-lower-upper-cut-ℝ :
-    is-in-lower-cut-ℝ x p →
-    is-in-upper-cut-ℝ x q →
-    le-ℚ p q
-  le-lower-upper-cut-ℝ H H' =
-    rec-coproduct
-      ( id)
-      ( λ I →
-        ex-falso
-          ( is-disjoint-cut-ℝ x p
-              ( H , leq-upper-cut-ℝ x q p I H')))
-      ( decide-le-leq-ℚ p q)
+  abstract
+    le-lower-upper-cut-ℝ :
+      is-in-lower-cut-ℝ x p →
+      is-in-upper-cut-ℝ x q →
+      le-ℚ p q
+    le-lower-upper-cut-ℝ H H' =
+      rec-coproduct
+        ( id)
+        ( λ I →
+          ex-falso
+            ( is-disjoint-cut-ℝ x p
+                ( H , leq-upper-cut-ℝ x q p I H')))
+        ( decide-le-leq-ℚ p q)
+
+    leq-lower-upper-cut-ℝ :
+      is-in-lower-cut-ℝ x p →
+      is-in-upper-cut-ℝ x q →
+      leq-ℚ p q
+    leq-lower-upper-cut-ℝ H H' = leq-le-ℚ (le-lower-upper-cut-ℝ H H')
 ```
 
 ### Characterization of each cut by the other
@@ -513,6 +523,46 @@ module _
   eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y)
 ```
 
+### The maximum of two elements of a lower cut of a real number is in the lower cut
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    is-in-lower-cut-max-ℚ :
+      (p q : ℚ) → is-in-lower-cut-ℝ x p → is-in-lower-cut-ℝ x q →
+      is-in-lower-cut-ℝ x (max-ℚ p q)
+    is-in-lower-cut-max-ℚ p q p<x q<x =
+      rec-coproduct
+        ( λ p≤q →
+          inv-tr (is-in-lower-cut-ℝ x) (left-leq-right-max-ℚ p q p≤q) q<x)
+        ( λ q≤p →
+          inv-tr (is-in-lower-cut-ℝ x) (right-leq-left-max-ℚ p q q≤p) p<x)
+        ( linear-leq-ℚ p q)
+```
+
+### The minimum of two elements of a upper cut of a real number is in the upper cut
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    is-in-upper-cut-min-ℚ :
+      (p q : ℚ) → is-in-upper-cut-ℝ x p → is-in-upper-cut-ℝ x q →
+      is-in-upper-cut-ℝ x (min-ℚ p q)
+    is-in-upper-cut-min-ℚ p q x<p x<q =
+      rec-coproduct
+        ( λ p≤q →
+          inv-tr (is-in-upper-cut-ℝ x) (left-leq-right-min-ℚ p q p≤q) x<p)
+        ( λ q≤p →
+          inv-tr (is-in-upper-cut-ℝ x) (right-leq-left-min-ℚ p q q≤p) x<q)
+        ( linear-leq-ℚ p q)
+```
+
 ## References
 
 This page follows parts of Section 11.2 in {{#cite UF13}}.
diff --git a/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md b/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md
new file mode 100644
index 0000000000..1f9272b8db
--- /dev/null
+++ b/src/real-numbers/enclosing-closed-rational-intervals-real-numbers.lagda.md
@@ -0,0 +1,168 @@
+# Enclosing closed rational intervals of Dedekind real numbers
+
+```agda
+module real-numbers.enclosing-closed-rational-intervals-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.interior-closed-intervals-rational-numbers
+open import elementary-number-theory.intersections-closed-intervals-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.conjunction
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.inhabited-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+An enclosing
+[closed rational interval](elementary-number-theory.closed-intervals-rational-numbers.md)
+of a [Dedekind real number](real-numbers.dedekind-real-numbers.md) `x` is a
+closed interval of rational numbers whose lower bound is in the lower cut of `x`
+and whose upper count is in the upper cut of `x`.
+
+## Definition
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  enclosing-closed-rational-interval-ℝ : subtype l closed-interval-ℚ
+  enclosing-closed-rational-interval-ℝ ((p , q) , _) =
+    lower-cut-ℝ x p ∧ upper-cut-ℝ x q
+
+  is-enclosing-closed-rational-interval-ℝ : closed-interval-ℚ → UU l
+  is-enclosing-closed-rational-interval-ℝ [p,q] =
+    type-Prop (enclosing-closed-rational-interval-ℝ [p,q])
+
+  type-enclosing-closed-rational-interval-ℝ : UU l
+  type-enclosing-closed-rational-interval-ℝ =
+    type-subtype enclosing-closed-rational-interval-ℝ
+```
+
+## Properties
+
+### There exists a rational enclosing interval around each real number
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    is-inhabited-type-enclosing-closed-rational-interval-ℝ :
+      is-inhabited (type-enclosing-closed-rational-interval-ℝ x)
+    is-inhabited-type-enclosing-closed-rational-interval-ℝ =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( is-inhabited-Prop (type-enclosing-closed-rational-interval-ℝ x))
+      in do
+        (p , p<x) ← is-inhabited-lower-cut-ℝ x
+        (q , x<q) ← is-inhabited-upper-cut-ℝ x
+        intro-exists
+          ( (p , q) , leq-lower-upper-cut-ℝ x p q p<x x<q)
+          ( p<x , x<q)
+```
+
+### For any rational enclosing interval around a real number, there exists an interior enclosing interval
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    exists-interior-enclosing-closed-rational-interval-ℝ :
+      ([a,b] : closed-interval-ℚ) →
+      is-enclosing-closed-rational-interval-ℝ x [a,b] →
+      exists
+        ( closed-interval-ℚ)
+        ( λ [c,d] →
+          enclosing-closed-rational-interval-ℝ x [c,d] ∧
+          is-interior-prop-closed-interval-ℚ [a,b] [c,d])
+    exists-interior-enclosing-closed-rational-interval-ℝ
+      [a,b]@((a , b) , _) (a<x , x<b) =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( closed-interval-ℚ)
+              ( λ [c,d] →
+                enclosing-closed-rational-interval-ℝ x [c,d] ∧
+                is-interior-prop-closed-interval-ℚ [a,b] [c,d]))
+      in do
+        (a' , a<a' , a'<x) ←
+          forward-implication (is-rounded-lower-cut-ℝ x a) a<x
+        (b' , b'<b , x<b') ←
+          forward-implication (is-rounded-upper-cut-ℝ x b) x<b
+        intro-exists
+          ( (a' , b') , leq-lower-upper-cut-ℝ x a' b' a'<x x<b')
+          ( ( a'<x , x<b') , (a<a' , b'<b))
+```
+
+### Any two rational enclosing intervals around a real number intersect
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    intersect-enclosing-closed-rational-interval-ℝ :
+      ([a,b] [c,d] : closed-interval-ℚ) →
+      is-enclosing-closed-rational-interval-ℝ x [a,b] →
+      is-enclosing-closed-rational-interval-ℝ x [c,d] →
+      intersect-closed-interval-ℚ [a,b] [c,d]
+    intersect-enclosing-closed-rational-interval-ℝ
+      [a,b]@((a , b) , _) [c,d]@((c , d) , _) (a<x , x<b) (c<x , x<d) =
+      ( leq-lower-upper-cut-ℝ x a d a<x x<d ,
+        leq-lower-upper-cut-ℝ x c b c<x x<b)
+
+    is-enclosing-intersection-enclosing-closed-rational-interval-ℝ :
+      ([a,b] [c,d] : closed-interval-ℚ) →
+      (H : is-enclosing-closed-rational-interval-ℝ x [a,b]) →
+      (K : is-enclosing-closed-rational-interval-ℝ x [c,d]) →
+      is-enclosing-closed-rational-interval-ℝ
+        ( x)
+        ( intersection-closed-interval-ℚ [a,b] [c,d]
+          ( intersect-enclosing-closed-rational-interval-ℝ [a,b] [c,d] H K))
+    is-enclosing-intersection-enclosing-closed-rational-interval-ℝ
+      ( (a , b) , _) ((c , d) , _) (a<x , x<b) (c<x , x<d) =
+      ( is-in-lower-cut-max-ℚ x a c a<x c<x ,
+        is-in-upper-cut-min-ℚ x b d x<b x<d)
+
+  intersection-type-enclosing-closed-rational-interval-ℝ :
+    type-enclosing-closed-rational-interval-ℝ x →
+    type-enclosing-closed-rational-interval-ℝ x →
+    type-enclosing-closed-rational-interval-ℝ x
+  intersection-type-enclosing-closed-rational-interval-ℝ
+    ( [a,b] , H) ([c,d] , K) =
+    ( intersection-closed-interval-ℚ [a,b] [c,d]
+        ( intersect-enclosing-closed-rational-interval-ℝ [a,b] [c,d] H K) ,
+      is-enclosing-intersection-enclosing-closed-rational-interval-ℝ
+        ( [a,b])
+        ( [c,d])
+        ( H)
+        ( K))
+```
diff --git a/src/real-numbers/multiplication-real-numbers.lagda.md b/src/real-numbers/multiplication-real-numbers.lagda.md
new file mode 100644
index 0000000000..7eb3b7277c
--- /dev/null
+++ b/src/real-numbers/multiplication-real-numbers.lagda.md
@@ -0,0 +1,1137 @@
+# Multiplication of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.multiplication-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.addition-closed-intervals-rational-numbers
+open import elementary-number-theory.addition-positive-rational-numbers
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.intersections-closed-intervals-rational-numbers
+open import elementary-number-theory.maximum-natural-numbers
+open import elementary-number-theory.maximum-nonnegative-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.minimum-positive-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.multiplication-closed-intervals-rational-numbers
+open import elementary-number-theory.multiplication-interior-closed-intervals-rational-numbers
+open import elementary-number-theory.multiplication-nonnegative-rational-numbers
+open import elementary-number-theory.multiplication-positive-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.nonzero-natural-numbers
+open import elementary-number-theory.poset-closed-intervals-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-positive-rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+open import elementary-number-theory.unit-fractions-rational-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.disjoint-subtypes
+open import foundation.empty-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.inhabited-subtypes
+open import foundation.logical-equivalences
+open import foundation.powersets
+open import foundation.propositional-truncations
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import logic.functoriality-existential-quantification
+
+open import order-theory.large-posets
+open import order-theory.posets
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.arithmetically-located-dedekind-cuts
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.enclosing-closed-rational-intervals-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.lower-dedekind-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.upper-dedekind-real-numbers
+```
+
+</details>
+
+We introduce
+{{#concept "multiplication" Disambiguation="real numbers" Agda=mul-ℝ WDID=Q40276 WD="multiplication"}}
+on the [Dedekind real numbers](real-numbers.dedekind-real-numbers.md) and derive
+its basic properties.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  lower-cut-mul-ℝ : subtype (l1 ⊔ l2) ℚ
+  lower-cut-mul-ℝ q =
+    ∃ ( type-enclosing-closed-rational-interval-ℝ x ×
+        type-enclosing-closed-rational-interval-ℝ y)
+      ( λ (([ax,bx] , _ , _) , ([ay,by] , _ , _)) →
+        is-below-prop-closed-interval-ℚ
+          ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+          ( q))
+
+  upper-cut-mul-ℝ : subtype (l1 ⊔ l2) ℚ
+  upper-cut-mul-ℝ q =
+    ∃ ( type-enclosing-closed-rational-interval-ℝ x ×
+        type-enclosing-closed-rational-interval-ℝ y)
+      ( λ (([ax,bx] , _ , _) , ([ay,by] , _ , _)) →
+        is-above-prop-closed-interval-ℚ
+          ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+          ( q))
+
+  lower-cut-mul-ℝ' : subtype (l1 ⊔ l2) ℚ
+  lower-cut-mul-ℝ' q =
+    ∃ ( type-enclosing-closed-rational-interval-ℝ x ×
+        type-enclosing-closed-rational-interval-ℝ y)
+      ( λ (([ax,bx] , _ , _) , ([ay,by] , _ , _)) →
+        leq-ℚ-Prop
+          ( q)
+          ( lower-bound-mul-closed-interval-ℚ [ax,bx] [ay,by]))
+
+  upper-cut-mul-ℝ' : subtype (l1 ⊔ l2) ℚ
+  upper-cut-mul-ℝ' q =
+    ∃ ( type-enclosing-closed-rational-interval-ℝ x ×
+        type-enclosing-closed-rational-interval-ℝ y)
+      ( λ (([ax,bx] , _ , _) , ([ay,by] , _ , _)) →
+        leq-ℚ-Prop
+          ( upper-bound-mul-closed-interval-ℚ [ax,bx] [ay,by])
+          ( q))
+
+  abstract
+    leq-lower-cut-mul-ℝ-lower-cut-mul-ℝ' : lower-cut-mul-ℝ ⊆ lower-cut-mul-ℝ'
+    leq-lower-cut-mul-ℝ-lower-cut-mul-ℝ' q = map-tot-exists ( λ _ → leq-le-ℚ)
+
+    leq-upper-cut-mul-ℝ-upper-cut-mul-ℝ' : upper-cut-mul-ℝ ⊆ upper-cut-mul-ℝ'
+    leq-upper-cut-mul-ℝ-upper-cut-mul-ℝ' q = map-tot-exists ( λ _ → leq-le-ℚ)
+
+    leq-lower-cut-mul-ℝ'-lower-cut-mul-ℝ : lower-cut-mul-ℝ' ⊆ lower-cut-mul-ℝ
+    leq-lower-cut-mul-ℝ'-lower-cut-mul-ℝ q q∈L' =
+      let open do-syntax-trunc-Prop (lower-cut-mul-ℝ q)
+      in do
+        ( ( ([a,b]@((a , b) , a≤b) , a<x , x<b) ,
+            ([c,d]@((c , d) , c≤d) , c<y , y<d)) ,
+          q≤[a,b][c,d]) ← q∈L'
+        ( [a',b']@( (a' , b') , _) , (a'<x , x<b') , (a<a' , b'<b)) ←
+          exists-interior-enclosing-closed-rational-interval-ℝ
+            ( x)
+            ( [a,b])
+            ( a<x , x<b)
+        ( [c',d']@( (c' , d') , _) , (c'<y , y<d') , (c<c' , d'<d)) ←
+          exists-interior-enclosing-closed-rational-interval-ℝ
+            ( y)
+            ( [c,d])
+            ( c<y , y<d)
+        intro-exists
+          ( ([a',b'] , a'<x , x<b') , ([c',d'] , c'<y , y<d'))
+          ( concatenate-leq-le-ℚ _ _ _
+            ( q≤[a,b][c,d])
+            ( le-lower-bound-mul-interior-closed-interval-ℚ
+              ( [a,b])
+              ( [c,d])
+              ( [a',b'])
+              ( [c',d'])
+              ( a<a' , b'<b)
+              ( c<c' , d'<d)
+              ( le-lower-upper-cut-ℝ x a' b' a'<x x<b')
+              ( le-lower-upper-cut-ℝ y c' d' c'<y y<d')))
+
+    leq-upper-cut-mul-ℝ'-upper-cut-mul-ℝ : upper-cut-mul-ℝ' ⊆ upper-cut-mul-ℝ
+    leq-upper-cut-mul-ℝ'-upper-cut-mul-ℝ q q∈U' =
+      let open do-syntax-trunc-Prop (upper-cut-mul-ℝ q)
+      in do
+        ( ( ([a,b]@((a , b) , a≤b) , a<x , x<b) ,
+            ([c,d]@((c , d) , c≤d) , c<y , y<d)) ,
+          [a,b][c,d]≤q) ← q∈U'
+        ( [a',b']@( (a' , b') , _) , (a'<x , x<b') , (a<a' , b'<b)) ←
+          exists-interior-enclosing-closed-rational-interval-ℝ
+            ( x)
+            ( [a,b])
+            ( a<x , x<b)
+        ( [c',d']@( (c' , d') , _) , (c'<y , y<d') , (c<c' , d'<d)) ←
+          exists-interior-enclosing-closed-rational-interval-ℝ
+            ( y)
+            ( [c,d])
+            ( c<y , y<d)
+        intro-exists
+          ( ([a',b'] , a'<x , x<b') , ([c',d'] , c'<y , y<d'))
+          ( concatenate-le-leq-ℚ _ _ _
+            ( le-upper-bound-mul-interior-closed-interval-ℚ
+              ( [a,b])
+              ( [c,d])
+              ( [a',b'])
+              ( [c',d'])
+              ( a<a' , b'<b)
+              ( c<c' , d'<d)
+              ( le-lower-upper-cut-ℝ x a' b' a'<x x<b')
+              ( le-lower-upper-cut-ℝ y c' d' c'<y y<d'))
+            ( [a,b][c,d]≤q))
+
+    eq-lower-cut-mul-ℝ' : lower-cut-mul-ℝ ＝ lower-cut-mul-ℝ'
+    eq-lower-cut-mul-ℝ' =
+      eq-sim-subtype _ _
+        ( leq-lower-cut-mul-ℝ-lower-cut-mul-ℝ' ,
+          leq-lower-cut-mul-ℝ'-lower-cut-mul-ℝ)
+
+    eq-upper-cut-mul-ℝ' : upper-cut-mul-ℝ ＝ upper-cut-mul-ℝ'
+    eq-upper-cut-mul-ℝ' =
+      eq-sim-subtype _ _
+        ( leq-upper-cut-mul-ℝ-upper-cut-mul-ℝ' ,
+          leq-upper-cut-mul-ℝ'-upper-cut-mul-ℝ)
+
+    is-inhabited-lower-cut-mul-ℝ : is-inhabited-subtype lower-cut-mul-ℝ
+    is-inhabited-lower-cut-mul-ℝ =
+      let
+        open do-syntax-trunc-Prop (is-inhabited-subtype-Prop lower-cut-mul-ℝ')
+      in
+        inv-tr
+          ( is-inhabited-subtype)
+          ( eq-lower-cut-mul-ℝ')
+          ( do
+            a<x<b@([a,b] , _ , _) ←
+              is-inhabited-type-enclosing-closed-rational-interval-ℝ x
+            c<y<d@([c,d] , _ , _) ←
+              is-inhabited-type-enclosing-closed-rational-interval-ℝ y
+            intro-exists
+              ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
+              ( intro-exists (a<x<b , c<y<d) (refl-leq-ℚ _)))
+
+    is-inhabited-upper-cut-mul-ℝ : is-inhabited-subtype upper-cut-mul-ℝ
+    is-inhabited-upper-cut-mul-ℝ =
+      let
+        open do-syntax-trunc-Prop (is-inhabited-subtype-Prop upper-cut-mul-ℝ')
+      in
+        inv-tr
+          ( is-inhabited-subtype)
+          ( eq-upper-cut-mul-ℝ')
+          ( do
+            a<x<b@([a,b] , _ , _) ←
+              is-inhabited-type-enclosing-closed-rational-interval-ℝ x
+            c<y<d@([c,d] , _ , _) ←
+              is-inhabited-type-enclosing-closed-rational-interval-ℝ y
+            intro-exists
+              ( upper-bound-mul-closed-interval-ℚ [a,b] [c,d])
+              ( intro-exists (a<x<b , c<y<d) (refl-leq-ℚ _)))
+
+    forward-implication-is-rounded-lower-cut-mul-ℝ :
+      (q : ℚ) → is-in-subtype lower-cut-mul-ℝ q →
+      exists ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-mul-ℝ r)
+    forward-implication-is-rounded-lower-cut-mul-ℝ q q∈L =
+      let
+        open
+          do-syntax-trunc-Prop (∃ ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-mul-ℝ r))
+      in do
+        ((a<x<b , c<y<d) , q<[a,b][c,d]) ← q∈L
+        (r , q<r , r<[a,b][c,d]) ← dense-le-ℚ q _ q<[a,b][c,d]
+        intro-exists r (q<r , intro-exists (a<x<b , c<y<d) r<[a,b][c,d])
+
+    forward-implication-is-rounded-upper-cut-mul-ℝ :
+      (r : ℚ) → is-in-subtype upper-cut-mul-ℝ r →
+      exists ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-mul-ℝ q)
+    forward-implication-is-rounded-upper-cut-mul-ℝ r r∈U =
+      let
+        open
+          do-syntax-trunc-Prop (∃ ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-mul-ℝ q))
+      in do
+        ((a<x<b , c<y<d) , [a,b][c,d]<r) ← r∈U
+        (q , [a,b][c,d]<q , q<r) ← dense-le-ℚ _ r [a,b][c,d]<r
+        intro-exists q (q<r , intro-exists (a<x<b , c<y<d) [a,b][c,d]<q)
+
+    backward-implication-is-rounded-lower-cut-mul-ℝ :
+      (q : ℚ) → exists ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-mul-ℝ r) →
+      is-in-subtype lower-cut-mul-ℝ q
+    backward-implication-is-rounded-lower-cut-mul-ℝ q ∃r =
+      let open do-syntax-trunc-Prop (lower-cut-mul-ℝ q)
+      in do
+        (r , q<r , r∈L) ← ∃r
+        ((a<x<b , c<y<d) , r<[a,b][c,d]) ← r∈L
+        intro-exists (a<x<b , c<y<d) (transitive-le-ℚ _ _ _ r<[a,b][c,d] q<r)
+
+    backward-implication-is-rounded-upper-cut-mul-ℝ :
+      (r : ℚ) → exists ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-mul-ℝ q) →
+      is-in-subtype upper-cut-mul-ℝ r
+    backward-implication-is-rounded-upper-cut-mul-ℝ r ∃q =
+      let open do-syntax-trunc-Prop (upper-cut-mul-ℝ r)
+      in do
+        (q , q<r , q∈U) ← ∃q
+        ((a<x<b , c<y<d) , [a,b][c,d]<q) ← q∈U
+        intro-exists (a<x<b , c<y<d) (transitive-le-ℚ _ _ _ q<r [a,b][c,d]<q)
+
+    is-rounded-lower-cut-mul-ℝ :
+      (q : ℚ) →
+      ( is-in-subtype lower-cut-mul-ℝ q ↔
+        exists ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-mul-ℝ r))
+    is-rounded-lower-cut-mul-ℝ q =
+      ( forward-implication-is-rounded-lower-cut-mul-ℝ q ,
+        backward-implication-is-rounded-lower-cut-mul-ℝ q)
+
+    is-rounded-upper-cut-mul-ℝ :
+      (r : ℚ) →
+      ( is-in-subtype upper-cut-mul-ℝ r ↔
+        exists ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-mul-ℝ q))
+    is-rounded-upper-cut-mul-ℝ r =
+      ( forward-implication-is-rounded-upper-cut-mul-ℝ r ,
+        backward-implication-is-rounded-upper-cut-mul-ℝ r)
+
+    is-disjoint-lower-upper-cut-mul-ℝ :
+      disjoint-subtype lower-cut-mul-ℝ upper-cut-mul-ℝ
+    is-disjoint-lower-upper-cut-mul-ℝ q (q∈L , q∈U) =
+      let open do-syntax-trunc-Prop empty-Prop
+      in do
+        ( ( a<x<b@([a,b]@((a , b) , a≤b) , a<x , x<b) ,
+            c<y<d@([c,d]@((c , d) , c≤d) , c<y , y<d)) ,
+          q<[a,b][c,d]) ← q∈L
+        ( ( a'<x<b'@([a',b']@((a' , b') , a'≤b') , a'<x , x<b') ,
+            c'<y<d'@([c',d']@((c' , d') , c'≤d') , c'<y , y<d')) ,
+          [a',b'][c',d']<q) ← q∈U
+        let
+          a'' = max-ℚ a a'
+          c'' = max-ℚ c c'
+        irreflexive-le-ℚ
+          ( q)
+          ( transitive-le-ℚ
+            ( q)
+            ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
+            ( q)
+            ( concatenate-leq-le-ℚ
+              ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
+              ( upper-bound-mul-closed-interval-ℚ [a',b'] [c',d'])
+              ( q)
+              ( transitive-leq-ℚ
+                ( lower-bound-mul-closed-interval-ℚ [a,b] [c,d])
+                ( a'' *ℚ c'')
+                ( upper-bound-mul-closed-interval-ℚ [a',b'] [c',d'])
+                ( pr2
+                  ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                    ( [a',b'])
+                    ( [c',d'])
+                    ( a'')
+                    ( c'')
+                    ( leq-right-max-ℚ a a' ,
+                      leq-max-leq-both-ℚ b' a a'
+                        ( leq-lower-upper-cut-ℝ x a b' a<x x<b')
+                        ( a'≤b'))
+                    ( leq-right-max-ℚ c c' ,
+                      leq-max-leq-both-ℚ d' c c'
+                        ( leq-lower-upper-cut-ℝ y c d' c<y y<d')
+                        ( c'≤d'))))
+                ( pr1
+                  ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                    ( [a,b])
+                    ( [c,d])
+                    ( a'')
+                    ( c'')
+                    ( leq-left-max-ℚ a a' ,
+                      leq-max-leq-both-ℚ b a a'
+                        ( a≤b)
+                        ( leq-lower-upper-cut-ℝ x a' b a'<x x<b))
+                    ( leq-left-max-ℚ c c' ,
+                      leq-max-leq-both-ℚ d c c'
+                        ( c≤d)
+                        ( leq-lower-upper-cut-ℝ y c' d c'<y y<d)))))
+              ( [a',b'][c',d']<q))
+            ( q<[a,b][c,d]))
+
+  lower-real-mul-ℝ : lower-ℝ (l1 ⊔ l2)
+  lower-real-mul-ℝ =
+    ( lower-cut-mul-ℝ ,
+      is-inhabited-lower-cut-mul-ℝ ,
+      is-rounded-lower-cut-mul-ℝ)
+
+  upper-real-mul-ℝ : upper-ℝ (l1 ⊔ l2)
+  upper-real-mul-ℝ =
+    ( upper-cut-mul-ℝ ,
+      is-inhabited-upper-cut-mul-ℝ ,
+      is-rounded-upper-cut-mul-ℝ)
+```
+
+To show the product of two real numbers is (weakly) arithmetically located, we
+use that the bound of the width of the interval product `[a, b] ∙ [c, d]` is at
+most
+
+$$
+(b - a) ·
+\max(\left\lvert c\right\rvert , \left\lvert d\right\rvert ) +
+(d - c) · \max(\left\lvert a\right\rvert , \left\lvert b\right\rvert )
+$$
+
+It suffices to exhibit intervals `[a, b]` around `x` and `[c, d]` around `y`
+such that this width is at most `ε`. We pick natural `Nx` such that if `[a, b]`
+is an interval around `x` and `b - a < 1`, then `|a| ≤ Nx` and `|b| ≤ Nx`, and
+analogously for `Ny`. Then using arithmetic locatedness of `x` and `y`, we pick
+appropriately small `εx` and `εy` such that `εx Nx + εy Ny ≤ ε`, `εx ≤ 1`, and
+`εy ≤ 1`, choose `a < x < b < a + εx` and `c < y < d < c + εy`, and get the
+desired bound.
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  abstract
+    is-weakly-arithmetically-located-mul-ℝ :
+      is-weakly-arithmetically-located-lower-upper-ℝ
+        ( lower-real-mul-ℝ x y)
+        ( upper-real-mul-ℝ x y)
+    is-weakly-arithmetically-located-mul-ℝ ε =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( ℚ × ℚ)
+              ( weak-close-bounds-lower-upper-ℝ
+                ( lower-real-mul-ℝ x y)
+                ( upper-real-mul-ℝ x y)
+                ( ε)))
+      in do
+        (Nx , bound-Nx) ← natural-bound-location-ℝ x one-ℚ⁺
+        (Ny , bound-Ny) ← natural-bound-location-ℝ y one-ℚ⁺
+        let
+          N = max-ℕ Nx Ny
+          (εx₀ , εy₀ , εx₀+εy₀=ε) = split-ℚ⁺ ε
+          εx =
+            min-ℚ⁺
+              ( one-ℚ⁺)
+              ( εx₀ *ℚ⁺ positive-reciprocal-rational-succ-ℕ N)
+          εy =
+            min-ℚ⁺
+              ( one-ℚ⁺)
+              ( εy₀ *ℚ⁺ positive-reciprocal-rational-succ-ℕ N)
+        ((p , q) , q<p+εx , p<x , x<q) ← is-arithmetically-located-ℝ x εx
+        ((r , s) , s<r+εy , r<y , y<s) ← is-arithmetically-located-ℝ y εy
+        let
+          p≤q = leq-lower-upper-cut-ℝ x p q p<x x<q
+          r≤s = leq-lower-upper-cut-ℝ y r s r<y y<s
+          q-p<εx : le-ℚ (q -ℚ p) (rational-ℚ⁺ εx)
+          q-p<εx =
+            le-transpose-right-add-ℚ _ _ _
+              ( tr (le-ℚ q) (commutative-add-ℚ _ _) q<p+εx)
+          q-p<1 =
+            concatenate-le-leq-ℚ
+              ( q -ℚ p)
+              ( rational-ℚ⁺ εx)
+              ( one-ℚ)
+              ( q-p<εx)
+              ( leq-left-min-ℚ⁺ _ _)
+          s-r<εy : le-ℚ (s -ℚ r) (rational-ℚ⁺ εy)
+          s-r<εy =
+            le-transpose-right-add-ℚ _ _ _
+              ( tr (le-ℚ s) (commutative-add-ℚ _ _) s<r+εy)
+          s-r<1 =
+            concatenate-le-leq-ℚ
+              ( s -ℚ r)
+              ( rational-ℚ⁺ εy)
+              ( one-ℚ)
+              ( s-r<εy)
+              ( leq-left-min-ℚ⁺ _ _)
+          open inequality-reasoning-Poset ℚ-Poset
+          max|r||s|≤sN =
+            chain-of-inequalities
+              max-ℚ (rational-abs-ℚ r) (rational-abs-ℚ s)
+              ≤ rational-ℕ Ny
+                by
+                  leq-le-ℚ
+                    ( bound-Ny
+                      ( (r , s) ,
+                        tr
+                          ( le-ℚ s)
+                          ( commutative-add-ℚ _ _)
+                          ( le-transpose-left-diff-ℚ _ _ _ s-r<1) ,
+                        r<y ,
+                        y<s))
+              ≤ rational-ℕ N
+                by preserves-leq-rational-ℕ _ _ (right-leq-max-ℕ _ _)
+              ≤ rational-ℕ (succ-ℕ N)
+                by preserves-leq-rational-ℕ _ _ (succ-leq-ℕ N)
+          max|p||q|≤sN =
+            chain-of-inequalities
+              max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q)
+              ≤ rational-ℕ Nx
+                by
+                  leq-le-ℚ
+                    ( bound-Nx
+                      ( (p , q) ,
+                        tr
+                          ( le-ℚ q)
+                          ( commutative-add-ℚ _ _)
+                          ( le-transpose-left-diff-ℚ _ _ _ q-p<1) ,
+                        p<x ,
+                        x<q))
+              ≤ rational-ℕ N
+                by preserves-leq-rational-ℕ _ _ (left-leq-max-ℕ _ _)
+              ≤ rational-ℕ (succ-ℕ N)
+                by preserves-leq-rational-ℕ _ _ (succ-leq-ℕ N)
+          [p,q] = ((p , q) , p≤q)
+          [r,s] = ((r , s) , r≤s)
+          a = lower-bound-mul-closed-interval-ℚ [p,q] [r,s]
+          b = upper-bound-mul-closed-interval-ℚ [p,q] [r,s]
+          b-a≤ε =
+            chain-of-inequalities
+              b -ℚ a
+              ≤ ( (q -ℚ p) *ℚ
+                  max-ℚ (rational-abs-ℚ r) (rational-abs-ℚ s)) +ℚ
+                ( (s -ℚ r) *ℚ
+                  max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+                by bound-width-mul-closed-interval-ℚ [p,q] [r,s]
+              ≤ ( rational-ℚ⁺ εx *ℚ rational-ℕ (succ-ℕ N)) +ℚ
+                ( rational-ℚ⁺ εy *ℚ rational-ℕ (succ-ℕ N))
+                by
+                  preserves-leq-add-ℚ
+                    ( preserves-leq-mul-ℚ⁰⁺
+                      ( nonnegative-diff-leq-ℚ _ _ p≤q)
+                      ( nonnegative-ℚ⁺ εx)
+                      ( max-ℚ⁰⁺ (abs-ℚ r) (abs-ℚ s))
+                      ( nonnegative-rational-ℕ (succ-ℕ N))
+                      ( leq-le-ℚ q-p<εx)
+                      ( max|r||s|≤sN))
+                    ( preserves-leq-mul-ℚ⁰⁺
+                      ( nonnegative-diff-leq-ℚ _ _ r≤s)
+                      ( nonnegative-ℚ⁺ εy)
+                      ( max-ℚ⁰⁺ (abs-ℚ p) (abs-ℚ q))
+                      ( nonnegative-rational-ℕ (succ-ℕ N))
+                      ( leq-le-ℚ s-r<εy)
+                      ( max|p||q|≤sN))
+              ≤ ( rational-ℚ⁺ εx +ℚ rational-ℚ⁺ εy) *ℚ
+                rational-ℕ (succ-ℕ N)
+                by
+                  leq-eq-ℚ _ _
+                    ( inv (right-distributive-mul-add-ℚ _ _ _))
+              ≤ rational-ℚ⁺
+                  ( ( εx₀ *ℚ⁺ positive-reciprocal-rational-succ-ℕ N) +ℚ⁺
+                    ( εy₀ *ℚ⁺ positive-reciprocal-rational-succ-ℕ N)) *ℚ
+                  ( rational-ℕ (succ-ℕ N))
+                by
+                  preserves-leq-right-mul-ℚ⁰⁺
+                    ( nonnegative-rational-ℕ (succ-ℕ N))
+                    ( _)
+                    ( _)
+                    ( preserves-leq-add-ℚ
+                      ( leq-right-min-ℚ⁺ _ _)
+                      ( leq-right-min-ℚ⁺ _ _))
+              ≤ rational-ℚ⁺ ε
+                by
+                  leq-eq-ℚ _ _
+                    ( ap-mul-ℚ
+                      ( inv (right-distributive-mul-add-ℚ _ _ _))
+                      ( refl) ∙
+                      ap
+                        ( rational-ℚ⁺)
+                        ( is-section-right-mul-ℚ⁺
+                          ( positive-rational-ℕ⁺ (succ-nonzero-ℕ' N))
+                          ( εx₀ +ℚ⁺ εy₀) ∙
+                          εx₀+εy₀=ε))
+        intro-exists
+          ( a , b)
+          ( tr
+              ( leq-ℚ b)
+              ( commutative-add-ℚ _ _)
+              ( leq-transpose-left-diff-ℚ _ _ _ b-a≤ε) ,
+            leq-lower-cut-mul-ℝ'-lower-cut-mul-ℝ x y a
+              ( intro-exists
+                ( (([p,q] , p<x , x<q)) , ([r,s] , r<y , y<s))
+                ( refl-leq-ℚ _)) ,
+            leq-upper-cut-mul-ℝ'-upper-cut-mul-ℝ x y b
+              ( intro-exists
+                ( (([p,q] , p<x , x<q)) , ([r,s] , r<y , y<s))
+                ( refl-leq-ℚ _)))
+
+  abstract
+    is-located-mul-ℝ :
+      is-located-lower-upper-ℝ (lower-real-mul-ℝ x y) (upper-real-mul-ℝ x y)
+    is-located-mul-ℝ =
+      is-located-is-weakly-arithmetically-located-lower-upper-ℝ _ _
+        ( is-weakly-arithmetically-located-mul-ℝ)
+
+  opaque
+    mul-ℝ : ℝ (l1 ⊔ l2)
+    mul-ℝ =
+      real-lower-upper-ℝ
+        ( lower-real-mul-ℝ x y)
+        ( upper-real-mul-ℝ x y)
+        ( is-disjoint-lower-upper-cut-mul-ℝ x y)
+        ( is-located-mul-ℝ)
+
+infixl 40 _*ℝ_
+_*ℝ_ : {l1 l2 : Level} → ℝ l1 → ℝ l2 → ℝ (l1 ⊔ l2)
+_*ℝ_ = mul-ℝ
+
+ap-mul-ℝ :
+  {l1 : Level} {x x' : ℝ l1} → (x ＝ x') →
+  {l2 : Level} {y y' : ℝ l2} → (y ＝ y') →
+  (x *ℝ y) ＝ (x' *ℝ y')
+ap-mul-ℝ x=x' y=y' = ap-binary mul-ℝ x=x' y=y'
+```
+
+## Properties
+
+### If `[a,b]` is an enclosing rational range of `xy`, then there are `ax < x < bx` and `ay < y < by` such that `a` is below `[ax, bx][ay, by]` and `b` is above it
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  opaque
+    unfolding mul-ℝ
+
+    enclosing-rational-range-mul-ℝ :
+      ([a,b] : closed-interval-ℚ) →
+      is-enclosing-closed-rational-interval-ℝ (x *ℝ y) [a,b] →
+      exists
+        ( type-enclosing-closed-rational-interval-ℝ x ×
+          type-enclosing-closed-rational-interval-ℝ y)
+        ( λ (([ax,bx] , _) , ([ay,by] , _)) →
+          is-below-prop-closed-interval-ℚ
+            ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+            ( lower-bound-closed-interval-ℚ [a,b]) ∧
+          is-above-prop-closed-interval-ℚ
+            ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+            ( upper-bound-closed-interval-ℚ [a,b]))
+    enclosing-rational-range-mul-ℝ ((a , b) , _) (a<xy , xy<b) =
+      let
+        open
+          do-syntax-trunc-Prop
+            ( ∃
+              ( type-enclosing-closed-rational-interval-ℝ x ×
+                type-enclosing-closed-rational-interval-ℝ y)
+              ( λ (([ax,bx] , _) , ([ay,by] , _)) →
+                is-below-prop-closed-interval-ℚ
+                  ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+                  ( a) ∧
+                is-above-prop-closed-interval-ℚ
+                  ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+                  ( b)))
+      in do
+        ( ( ax<x<bx@([ax,bx]@((ax , bx) , _) , x∈⟨ax,bx⟩) ,
+            ay<y<by@([ay,by]@((ay , by) , _) , y∈⟨ay,by⟩)) ,
+          a<[ax,bx][ay,by]) ← a<xy
+        ( ( ax'<x<bx'@([ax',bx']@((ax' , bx') , _) , x∈⟨ax',bx'⟩) ,
+            ay'<y<by'@([ay',by']@((ay' , by') , _) , y∈⟨ay',by'⟩)) ,
+          [ax',bx'][ay',by']<b) ← xy<b
+        let
+          ax''<x<bx''@([ax'',bx''] , _) =
+            intersection-type-enclosing-closed-rational-interval-ℝ x
+              ( ax<x<bx)
+              ( ax'<x<bx')
+          ay''<y<by''@([ay'',by''] , _) =
+            intersection-type-enclosing-closed-rational-interval-ℝ y
+              ( ay<y<by)
+              ( ay'<y<by')
+          [ax,bx]∩[ax',bx'] =
+            intersect-enclosing-closed-rational-interval-ℝ
+              ( x)
+              ( [ax,bx])
+              ( [ax',bx'])
+              ( x∈⟨ax,bx⟩)
+              ( x∈⟨ax',bx'⟩)
+          [ay,by]∩[ay',by'] =
+            intersect-enclosing-closed-rational-interval-ℝ
+              ( y)
+              ( [ay,by])
+              ( [ay',by'])
+              ( y∈⟨ay,by⟩)
+              ( y∈⟨ay',by'⟩)
+          [ax'',bx''][ay'',by'']⊆[ax,bx][ay,by] =
+            preserves-leq-mul-closed-interval-ℚ
+              ( [ax'',bx''])
+              ( [ax,bx])
+              ( [ay'',by''])
+              ( [ay,by])
+              ( leq-left-intersection-closed-interval-ℚ
+                ( [ax,bx])
+                ( [ax',bx'])
+                ( [ax,bx]∩[ax',bx']))
+              ( leq-left-intersection-closed-interval-ℚ
+                ( [ay,by])
+                ( [ay',by'])
+                ( [ay,by]∩[ay',by']))
+          [ax'',bx''][ay'',by'']⊆[ax',bx'][ay',by'] =
+            preserves-leq-mul-closed-interval-ℚ
+              ( [ax'',bx''])
+              ( [ax',bx'])
+              ( [ay'',by''])
+              ( [ay',by'])
+              ( leq-right-intersection-closed-interval-ℚ
+                ( [ax,bx])
+                ( [ax',bx'])
+                ( [ax,bx]∩[ax',bx']))
+              ( leq-right-intersection-closed-interval-ℚ
+                ( [ay,by])
+                ( [ay',by'])
+                ( [ay,by]∩[ay',by']))
+        intro-exists
+          ( ax''<x<bx'' , ay''<y<by'')
+          ( concatenate-le-leq-ℚ _ _ _
+              ( a<[ax,bx][ay,by])
+              ( pr1 [ax'',bx''][ay'',by'']⊆[ax,bx][ay,by]) ,
+            concatenate-leq-le-ℚ _ _ _
+              ( pr2 [ax'',bx''][ay'',by'']⊆[ax',bx'][ay',by'])
+              ( [ax',bx'][ay',by']<b))
+```
+
+### Commutativity of multiplication
+
+```agda
+opaque
+  unfolding leq-ℝ mul-ℝ
+
+  leq-commute-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) →
+    leq-ℝ (x *ℝ y) (y *ℝ x)
+  leq-commute-ℝ x y q q<xy =
+    let open do-syntax-trunc-Prop (lower-cut-mul-ℝ y x q)
+    in do
+      ((a<x<b@([a,b] , _ , _) , c<y<d@([c,d] , _ , _)) , q<[a,b][c,d]) ← q<xy
+      intro-exists
+        ( c<y<d , a<x<b)
+        ( tr
+          ( λ [x,y] → is-below-closed-interval-ℚ [x,y] q)
+          ( commutative-mul-closed-interval-ℚ _ _)
+          ( q<[a,b][c,d]))
+
+abstract
+  commutative-mul-ℝ : {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → x *ℝ y ＝ y *ℝ x
+  commutative-mul-ℝ x y =
+    antisymmetric-leq-ℝ _ _ (leq-commute-ℝ x y) (leq-commute-ℝ y x)
+```
+
+### Associativity of multiplication
+
+```agda
+module _
+  {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
+  where
+
+  opaque
+    unfolding leq-ℝ mul-ℝ
+
+    leq-associative-mul-ℝ : leq-ℝ ((x *ℝ y) *ℝ z) (x *ℝ (y *ℝ z))
+    leq-associative-mul-ℝ q q<⟨xy⟩z =
+      let open do-syntax-trunc-Prop (lower-cut-mul-ℝ x (y *ℝ z) q)
+      in do
+        ( ( axy<xy<bxy@([axy,bxy]@((axy , bxy) , _) , axy<xy , xy<bxy) ,
+            az<z<bz@([az,bz]@((az , bz) , _) , z∈⟨az,bz⟩)) ,
+          q<[axy,bxy][az,bz]) ← q<⟨xy⟩z
+        ( ( ax<x<bx@([ax,bx]@((ax , bx) , _) , x∈⟨ax,bx⟩) ,
+            ay<y<by@([ay,by]@((ay , by) , _) , y∈⟨ay,by⟩)) ,
+          axy<[ax,bx][ay,by] , [ax,bx][ay,by]<bxy) ←
+          enclosing-rational-range-mul-ℝ x y [axy,bxy] (axy<xy , xy<bxy)
+        intro-exists
+          ( ax<x<bx ,
+            ( mul-closed-interval-ℚ [ay,by] [az,bz] ,
+              leq-lower-cut-mul-ℝ'-lower-cut-mul-ℝ y z
+                ( lower-bound-mul-closed-interval-ℚ [ay,by] [az,bz])
+                ( intro-exists (ay<y<by , az<z<bz) (refl-leq-ℚ _)) ,
+              leq-upper-cut-mul-ℝ'-upper-cut-mul-ℝ y z
+                ( upper-bound-mul-closed-interval-ℚ [ay,by] [az,bz])
+                ( intro-exists (ay<y<by , az<z<bz) (refl-leq-ℚ _))))
+          ( concatenate-le-leq-ℚ q _ _
+            ( q<[axy,bxy][az,bz])
+            ( pr1
+              ( tr
+                ( λ z →
+                  leq-closed-interval-ℚ
+                    ( z)
+                    ( mul-closed-interval-ℚ [axy,bxy] [az,bz]))
+                ( associative-mul-closed-interval-ℚ [ax,bx] [ay,by] [az,bz])
+                ( preserves-leq-left-mul-closed-interval-ℚ
+                  ( [az,bz])
+                  ( mul-closed-interval-ℚ [ax,bx] [ay,by])
+                  ( [axy,bxy])
+                  ( leq-le-ℚ axy<[ax,bx][ay,by] ,
+                    leq-le-ℚ [ax,bx][ay,by]<bxy)))))
+
+module _
+  {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
+  where
+
+  abstract
+    associative-mul-ℝ : (x *ℝ y) *ℝ z ＝ x *ℝ (y *ℝ z)
+    associative-mul-ℝ =
+      antisymmetric-leq-ℝ _ _
+        ( leq-associative-mul-ℝ x y z)
+        ( binary-tr
+          ( leq-ℝ)
+          ( ( commutative-mul-ℝ (z *ℝ y) x) ∙
+            ( ap-mul-ℝ refl (commutative-mul-ℝ z y)))
+          ( ( commutative-mul-ℝ z (y *ℝ x)) ∙
+            ( ap-mul-ℝ (commutative-mul-ℝ y x) refl))
+          ( leq-associative-mul-ℝ z y x))
+```
+
+### Unit laws
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  opaque
+    unfolding leq-ℝ leq-ℝ' mul-ℝ real-ℚ
+
+    leq-right-unit-law-mul-ℝ : leq-ℝ (x *ℝ one-ℝ) x
+    leq-right-unit-law-mul-ℝ q q<x1 =
+      let open do-syntax-trunc-Prop (lower-cut-ℝ x q)
+      in do
+        ( ( ax<x<bx@([ax,bx]@((ax , bx) , _) , ax<x , x<bx) ,
+            a₁<1<b₁@([a₁,b₁]@((a₁ , b₁) , _) , a₁<1 , 1<b₁)) ,
+          q<[ax,bx][a₁,b₁]) ← q<x1
+        le-lower-cut-ℝ x q ax
+          ( concatenate-le-leq-ℚ _ _ _
+            ( q<[ax,bx][a₁,b₁])
+            ( tr
+              ( leq-ℚ _)
+              ( right-unit-law-mul-ℚ ax)
+              ( pr1
+                ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                  ( [ax,bx])
+                  ( [a₁,b₁])
+                  ( ax)
+                  ( one-ℚ)
+                  ( lower-bound-is-in-closed-interval-ℚ [ax,bx])
+                  ( leq-le-ℚ a₁<1 , leq-le-ℚ 1<b₁)))))
+          ( ax<x)
+
+    leq-right-unit-law-mul-ℝ' : leq-ℝ x (x *ℝ one-ℝ)
+    leq-right-unit-law-mul-ℝ' =
+      leq-leq'-ℝ x (x *ℝ one-ℝ)
+        ( λ q x1<q →
+          let open do-syntax-trunc-Prop (upper-cut-ℝ x q)
+          in do
+            ( ( ax<x<bx@([ax,bx]@((ax , bx) , _) , ax<x , x<bx) ,
+                a₁<1<b₁@([a₁,b₁]@((a₁ , b₁) , _) , a₁<1 , 1<b₁)) ,
+              [ax,bx][a₁,b₁]<q) ← x1<q
+            le-upper-cut-ℝ x bx q
+              ( concatenate-leq-le-ℚ _ _ _
+                ( tr
+                  ( λ p →
+                    leq-ℚ p (upper-bound-mul-closed-interval-ℚ [ax,bx] [a₁,b₁]))
+                  ( right-unit-law-mul-ℚ bx)
+                  ( pr2
+                    ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                      ( [ax,bx])
+                      ( [a₁,b₁])
+                      ( bx)
+                      ( one-ℚ)
+                      ( upper-bound-is-in-closed-interval-ℚ [ax,bx])
+                      ( leq-le-ℚ a₁<1 , leq-le-ℚ 1<b₁))))
+                ( [ax,bx][a₁,b₁]<q))
+              ( x<bx))
+
+  abstract
+    right-unit-law-mul-ℝ : x *ℝ one-ℝ ＝ x
+    right-unit-law-mul-ℝ =
+      antisymmetric-leq-ℝ _ _ leq-right-unit-law-mul-ℝ leq-right-unit-law-mul-ℝ'
+
+    left-unit-law-mul-ℝ : one-ℝ *ℝ x ＝ x
+    left-unit-law-mul-ℝ = commutative-mul-ℝ one-ℝ x ∙ right-unit-law-mul-ℝ
+```
+
+### Distributivity of multiplication over addition
+
+```agda
+opaque
+  unfolding leq-ℝ leq-ℝ' mul-ℝ add-ℝ
+
+  leq-left-distributive-mul-add-ℝ :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    leq-ℝ (x *ℝ (y +ℝ z)) ((x *ℝ y) +ℝ (x *ℝ z))
+  leq-left-distributive-mul-add-ℝ x y z =
+    leq-leq'-ℝ (x *ℝ (y +ℝ z)) (x *ℝ y +ℝ x *ℝ z)
+      ( λ q xy+xz<q →
+        let open do-syntax-trunc-Prop (upper-cut-mul-ℝ x (y +ℝ z) q)
+        in do
+          ( (qxy , qxz) , xy<qxy , xz<qxz , q=qxy+qxz) ← xy+xz<q
+          ( ( ax<x<bx@([ax,bx] , x∈⟨ax,bx⟩) ,
+              ay<y<by@([ay,by]@((ay , by) , _) , ay<y , y<by)) ,
+            [ax,bx][ay,by]<qxy) ← xy<qxy
+          ( ( ax'<x<bx'@([ax',bx'] , x∈⟨ax',bx'⟩) ,
+              az<z<bz@([az,bz]@((az , bz) , _) , az<z , z<bz)) ,
+            [ax',bx'][az,bz]<qxz) ← xz<qxz
+          let
+            ax''<x<bx''@([ax'',bx''] , _) =
+              intersection-type-enclosing-closed-rational-interval-ℝ
+                ( x)
+                ( ax<x<bx)
+                ( ax'<x<bx')
+            [ax,bx]∩[ax',bx'] =
+              intersect-enclosing-closed-rational-interval-ℝ
+                ( x)
+                ( [ax,bx])
+                ( [ax',bx'])
+                ( x∈⟨ax,bx⟩)
+                ( x∈⟨ax',bx'⟩)
+          intro-exists
+            ( ax''<x<bx'' ,
+              ( add-closed-interval-ℚ [ay,by] [az,bz] ,
+                intro-exists (ay , az) (ay<y , az<z , refl) ,
+                intro-exists (by , bz) (y<by , z<bz , refl)))
+            ( concatenate-leq-le-ℚ _ _ _
+              ( pr2
+                ( left-subdistributive-mul-add-closed-interval-ℚ
+                  ( [ax'',bx''])
+                  ( [ay,by])
+                  ( [az,bz])))
+              ( inv-tr
+                ( le-ℚ _)
+                ( q=qxy+qxz)
+                ( preserves-le-add-ℚ
+                  ( concatenate-leq-le-ℚ _ _ _
+                    ( pr2
+                      ( preserves-leq-left-mul-closed-interval-ℚ
+                        ( [ay,by])
+                        ( [ax'',bx''])
+                        ( [ax,bx])
+                        ( leq-left-intersection-closed-interval-ℚ
+                          ( [ax,bx])
+                          ( [ax',bx'])
+                          ( [ax,bx]∩[ax',bx']))))
+                    ( [ax,bx][ay,by]<qxy))
+                  ( concatenate-leq-le-ℚ _ _ _
+                    ( pr2
+                      ( preserves-leq-left-mul-closed-interval-ℚ
+                        ( [az,bz])
+                        ( [ax'',bx''])
+                        ( [ax',bx'])
+                        ( leq-right-intersection-closed-interval-ℚ
+                          ( [ax,bx])
+                          ( [ax',bx'])
+                          ( [ax,bx]∩[ax',bx']))))
+                    ( [ax',bx'][az,bz]<qxz))))))
+
+  leq-left-distributive-mul-add-ℝ' :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    leq-ℝ ((x *ℝ y) +ℝ (x *ℝ z)) (x *ℝ (y +ℝ z))
+  leq-left-distributive-mul-add-ℝ' x y z q q<xy+xz =
+    let open do-syntax-trunc-Prop (lower-cut-mul-ℝ x (y +ℝ z) q)
+    in do
+      ( (qxy , qxz) , qxy<xy , qxz<xz , q=qxy+qxz) ← q<xy+xz
+      ( ( ax<x<bx@([ax,bx] , x∈⟨ax,bx⟩) ,
+          ay<y<by@([ay,by]@((ay , by) , _) , ay<y , y<by)) ,
+        qxy<[ax,bx][ay,by]) ← qxy<xy
+      ( ( ax'<x<bx'@([ax',bx'] , x∈⟨ax',bx'⟩) ,
+          az<z<bz@([az,bz]@((az , bz) , _) , az<z , z<bz)) ,
+        qxz<[ax',bx'][az,bz]) ← qxz<xz
+      let
+        ax''<x<bx''@([ax'',bx''] , _) =
+          intersection-type-enclosing-closed-rational-interval-ℝ
+            ( x)
+            ( ax<x<bx)
+            ( ax'<x<bx')
+        [ax,bx]∩[ax',bx'] =
+          intersect-enclosing-closed-rational-interval-ℝ
+            ( x)
+            ( [ax,bx])
+            ( [ax',bx'])
+            ( x∈⟨ax,bx⟩)
+            ( x∈⟨ax',bx'⟩)
+      intro-exists
+        ( ax''<x<bx'' ,
+          ( add-closed-interval-ℚ [ay,by] [az,bz] ,
+            intro-exists (ay , az) (ay<y , az<z , refl) ,
+            intro-exists (by , bz) (y<by , z<bz , refl)))
+        ( concatenate-le-leq-ℚ
+          ( q)
+          ( lower-bound-mul-closed-interval-ℚ [ax'',bx''] [ay,by] +ℚ
+            lower-bound-mul-closed-interval-ℚ [ax'',bx''] [az,bz])
+          ( lower-bound-mul-closed-interval-ℚ
+            ( [ax'',bx''])
+            ( add-closed-interval-ℚ [ay,by] [az,bz]))
+          ( inv-tr
+              ( λ p → le-ℚ p _)
+              ( q=qxy+qxz)
+              ( preserves-le-add-ℚ
+                ( concatenate-le-leq-ℚ _ _ _
+                  ( qxy<[ax,bx][ay,by])
+                  ( pr1
+                    ( preserves-leq-left-mul-closed-interval-ℚ
+                      ( [ay,by])
+                      ( [ax'',bx''])
+                      ( [ax,bx])
+                      ( leq-left-intersection-closed-interval-ℚ
+                        ( [ax,bx])
+                        ( [ax',bx'])
+                        ( [ax,bx]∩[ax',bx'])))))
+                ( concatenate-le-leq-ℚ _ _ _
+                  ( qxz<[ax',bx'][az,bz])
+                  ( pr1
+                    ( preserves-leq-left-mul-closed-interval-ℚ
+                      ( [az,bz])
+                      ( [ax'',bx''])
+                      ( [ax',bx'])
+                      ( leq-right-intersection-closed-interval-ℚ
+                        ( [ax,bx])
+                        ( [ax',bx'])
+                        ( [ax,bx]∩[ax',bx'])))))))
+          ( pr1
+            ( left-subdistributive-mul-add-closed-interval-ℚ
+              ( [ax'',bx''])
+              ( [ay,by])
+              ( [az,bz]))))
+
+abstract
+  left-distributive-mul-add-ℝ :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    x *ℝ (y +ℝ z) ＝ x *ℝ y +ℝ x *ℝ z
+  left-distributive-mul-add-ℝ x y z =
+    antisymmetric-leq-ℝ _ _
+      ( leq-left-distributive-mul-add-ℝ x y z)
+      ( leq-left-distributive-mul-add-ℝ' x y z)
+
+  right-distributive-mul-add-ℝ :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    (x +ℝ y) *ℝ z ＝ x *ℝ z +ℝ y *ℝ z
+  right-distributive-mul-add-ℝ x y z =
+    equational-reasoning
+      (x +ℝ y) *ℝ z
+      ＝ z *ℝ (x +ℝ y)
+        by commutative-mul-ℝ _ _
+      ＝ z *ℝ x +ℝ z *ℝ y
+        by left-distributive-mul-add-ℝ z x y
+      ＝ x *ℝ z +ℝ y *ℝ z
+        by ap-add-ℝ (commutative-mul-ℝ z x) (commutative-mul-ℝ z y)
+```
+
+### Zero laws
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  opaque
+    unfolding leq-ℝ leq-ℝ' mul-ℝ real-ℚ
+
+    leq-left-zero-law-mul-ℝ : leq-ℝ (zero-ℝ *ℝ x) zero-ℝ
+    leq-left-zero-law-mul-ℝ q q<0x =
+      let open do-syntax-trunc-Prop (le-ℚ-Prop q zero-ℚ)
+      in do
+        ( (([a₀,b₀] , a₀<0 , 0<b₀) , ([ax,bx]@((ax , bx) , _) , _)) ,
+          q<[a₀,b₀][ax,bx]) ← q<0x
+        concatenate-le-leq-ℚ
+          ( q)
+          ( lower-bound-mul-closed-interval-ℚ [a₀,b₀] [ax,bx])
+          ( zero-ℚ)
+          ( q<[a₀,b₀][ax,bx])
+          ( tr
+            ( leq-ℚ _)
+            ( left-zero-law-mul-ℚ ax)
+            ( pr1
+              ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                ( [a₀,b₀])
+                ( [ax,bx])
+                ( zero-ℚ)
+                ( ax)
+                ( leq-le-ℚ a₀<0 , leq-le-ℚ 0<b₀)
+                ( lower-bound-is-in-closed-interval-ℚ [ax,bx]))))
+
+    leq-left-zero-law-mul-ℝ' : leq-ℝ zero-ℝ (zero-ℝ *ℝ x)
+    leq-left-zero-law-mul-ℝ' =
+      leq-leq'-ℝ zero-ℝ (zero-ℝ *ℝ x)
+        ( λ q 0x<q →
+          let open do-syntax-trunc-Prop (le-ℚ-Prop zero-ℚ q)
+          in do
+            ( (([a₀,b₀] , a₀<0 , 0<b₀) , ([ax,bx]@((ax , bx) , _) , _)) ,
+              [a₀,b₀][ax,bx]<q) ← 0x<q
+            concatenate-leq-le-ℚ
+              ( zero-ℚ)
+              ( upper-bound-mul-closed-interval-ℚ [a₀,b₀] [ax,bx])
+              ( q)
+              ( tr
+                ( λ p →
+                  leq-ℚ p (upper-bound-mul-closed-interval-ℚ [a₀,b₀] [ax,bx]))
+                ( left-zero-law-mul-ℚ ax)
+                ( pr2
+                  ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                    ( [a₀,b₀])
+                    ( [ax,bx])
+                    ( zero-ℚ)
+                    ( ax)
+                    ( leq-le-ℚ a₀<0 , leq-le-ℚ 0<b₀)
+                    ( lower-bound-is-in-closed-interval-ℚ [ax,bx]))))
+              ( [a₀,b₀][ax,bx]<q))
+
+  abstract
+    left-zero-law-mul-ℝ : sim-ℝ (zero-ℝ *ℝ x) zero-ℝ
+    left-zero-law-mul-ℝ =
+      sim-sim-leq-ℝ (leq-left-zero-law-mul-ℝ , leq-left-zero-law-mul-ℝ')
+
+    right-zero-law-mul-ℝ : sim-ℝ (x *ℝ zero-ℝ) zero-ℝ
+    right-zero-law-mul-ℝ =
+      tr (λ y → sim-ℝ y zero-ℝ) (commutative-mul-ℝ _ _) left-zero-law-mul-ℝ
+```
+
+### The inclusion of rational numbers preserves multiplication
+
+```agda
+opaque
+  unfolding mul-ℝ real-ℚ
+
+  mul-real-ℚ : (p q : ℚ) → real-ℚ p *ℝ real-ℚ q ＝ real-ℚ (p *ℚ q)
+  mul-real-ℚ p q =
+    let open do-syntax-trunc-Prop empty-Prop
+    in
+      eq-sim-ℝ
+        ( sim-rational-ℝ
+          ( real-ℚ p *ℝ real-ℚ q ,
+            p *ℚ q ,
+            ( λ pq<pℝqℝ →
+                do
+                  ( (([a,b] , a<p , p<b) , ([c,d] , c<q , q<d)) ,
+                    pq<[a,b][c,d]) ← pq<pℝqℝ
+                  irreflexive-le-ℚ
+                    ( p *ℚ q)
+                    ( concatenate-le-leq-ℚ _ _ _
+                      ( pq<[a,b][c,d])
+                      ( pr1
+                        ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                          ( [a,b])
+                          ( [c,d])
+                          ( p)
+                          ( q)
+                          ( leq-le-ℚ a<p , leq-le-ℚ p<b)
+                          ( leq-le-ℚ c<q , leq-le-ℚ q<d))))) ,
+            ( λ pℝqℝ<pq →
+              do
+                ( (([a,b] , a<p , p<b) , ([c,d] , c<q , q<d)) ,
+                    [a,b][c,d]<pq) ← pℝqℝ<pq
+                irreflexive-le-ℚ
+                  ( p *ℚ q)
+                  ( concatenate-leq-le-ℚ _ _ _
+                    ( pr2
+                      ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                        ( [a,b])
+                        ( [c,d])
+                        ( p)
+                        ( q)
+                        ( leq-le-ℚ a<p , leq-le-ℚ p<b)
+                        ( leq-le-ℚ c<q , leq-le-ℚ q<d)))
+                    ( [a,b][c,d]<pq)))))
+```