diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index aecd69e5ec..815543ad14 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -33,6 +33,7 @@ open import elementary-number-theory.binomial-theorem-integers public
 open import elementary-number-theory.binomial-theorem-natural-numbers public
 open import elementary-number-theory.bounded-sums-arithmetic-functions public
 open import elementary-number-theory.catalan-numbers public
+open import elementary-number-theory.closed-intervals-rational-numbers public
 open import elementary-number-theory.cofibonacci public
 open import elementary-number-theory.collatz-bijection public
 open import elementary-number-theory.collatz-conjecture public
@@ -123,7 +124,9 @@ open import elementary-number-theory.multiplicative-units-integers public
 open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
+open import elementary-number-theory.negative-integer-fractions public
 open import elementary-number-theory.negative-integers public
+open import elementary-number-theory.negative-rational-numbers public
 open import elementary-number-theory.nonnegative-integers public
 open import elementary-number-theory.nonpositive-integers public
 open import elementary-number-theory.nonzero-integers public
diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md
new file mode 100644
index 0000000000..86535643cd
--- /dev/null
+++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md
@@ -0,0 +1,227 @@
+# Closed intervals of rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.closed-intervals-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.maximum-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.negative-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
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [rational number](elementary-number-theory.rational-numbers.md) `p` is in a
+{{#concept "closed interval" Disambiguation="rational numbers" WDID=Q78240777 WD="closed interval" Agda=closed-interval-ℚ}}
+`[q , r]` if `q` is
+[less than or equal to](elementary-number-theory.inequality-rational-numbers.md)
+`p` and `p` is less than or equal to `r`.
+
+## Definition
+
+```agda
+module _
+  (p q : ℚ)
+  where
+
+  closed-interval-ℚ : subtype lzero ℚ
+  closed-interval-ℚ r = (leq-ℚ-Prop p r) ∧ (leq-ℚ-Prop r q)
+
+  is-in-closed-interval-ℚ : ℚ → UU lzero
+  is-in-closed-interval-ℚ r = type-Prop (closed-interval-ℚ r)
+
+unordered-closed-interval-ℚ : ℚ → ℚ → subtype lzero ℚ
+unordered-closed-interval-ℚ p q = closed-interval-ℚ (min-ℚ p q) (max-ℚ p q)
+
+is-in-unordered-closed-interval-ℚ : ℚ → ℚ → ℚ → UU lzero
+is-in-unordered-closed-interval-ℚ p q =
+  is-in-closed-interval-ℚ (min-ℚ p q) (max-ℚ p q)
+
+is-in-unordered-closed-interval-is-in-closed-interval-ℚ :
+  (p q r : ℚ) →
+  is-in-closed-interval-ℚ p q r →
+  is-in-unordered-closed-interval-ℚ p q r
+is-in-unordered-closed-interval-is-in-closed-interval-ℚ p q r (p≤r , q≤r) =
+  transitive-leq-ℚ
+    ( min-ℚ p q)
+    ( p)
+    ( r)
+    ( p≤r)
+    ( leq-left-min-ℚ p q) ,
+  transitive-leq-ℚ
+    ( r)
+    ( q)
+    ( max-ℚ p q)
+    ( leq-right-max-ℚ p q)
+    ( q≤r)
+
+is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ :
+  (p q r : ℚ) → is-in-closed-interval-ℚ p q r →
+  is-in-unordered-closed-interval-ℚ q p r
+is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ
+  p q r (p≤r , q≤r) =
+  transitive-leq-ℚ
+    ( min-ℚ q p)
+    ( p)
+    ( r)
+    ( p≤r)
+    ( leq-right-min-ℚ q p) ,
+  transitive-leq-ℚ
+    ( r)
+    ( q)
+    ( max-ℚ q p)
+    ( leq-left-max-ℚ q p)
+    ( q≤r)
+```
+
+## Properties
+
+### Multiplication of elements in a closed interval
+
+```agda
+abstract
+  left-mul-negative-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r → is-negative-ℚ s →
+    is-in-closed-interval-ℚ (q *ℚ s) (p *ℚ s) (r *ℚ s)
+  left-mul-negative-closed-interval-ℚ p q r s (p≤r , r≤q) neg-s =
+    let
+      s⁻ = s , neg-s
+    in
+      reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q ,
+      reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r
+
+  left-mul-positive-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r → is-positive-ℚ s →
+    is-in-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s)
+  left-mul-positive-closed-interval-ℚ p q r s (p≤r , r≤q) pos-s =
+    let
+      s⁺ = s , pos-s
+    in
+      preserves-leq-right-mul-ℚ⁺ s⁺ p r p≤r ,
+      preserves-leq-right-mul-ℚ⁺ s⁺ r q r≤q
+
+  left-mul-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r →
+    is-in-unordered-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s)
+  left-mul-closed-interval-ℚ p q r s H@(p≤r , r≤q) =
+    let
+      p≤q = transitive-leq-ℚ p r q r≤q p≤r
+    in
+      trichotomy-le-ℚ
+        ( s)
+        ( zero-ℚ)
+        ( λ s<0 →
+          is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ
+            (q *ℚ s)
+            (p *ℚ s)
+            (r *ℚ s)
+            ( left-mul-negative-closed-interval-ℚ p q r s H
+              ( is-negative-le-zero-ℚ s s<0)))
+        ( λ s=0 →
+          let
+            ps=0 = ap (p *ℚ_) s=0 ∙ right-zero-law-mul-ℚ p
+            rs=0 = ap (r *ℚ_) s=0 ∙ right-zero-law-mul-ℚ r
+            qs=0 = ap (q *ℚ_) s=0 ∙ right-zero-law-mul-ℚ q
+          in
+            leq-eq-ℚ
+              ( _)
+              ( _)
+              ( ap-binary min-ℚ ps=0 qs=0 ∙
+                idempotent-min-ℚ zero-ℚ ∙ inv rs=0) ,
+            leq-eq-ℚ
+              ( _)
+              ( _)
+              ( rs=0 ∙
+                inv (ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ)))
+        ( λ 0<s →
+          is-in-unordered-closed-interval-is-in-closed-interval-ℚ
+            ( p *ℚ s)
+            ( q *ℚ s)
+            ( r *ℚ s)
+            ( left-mul-positive-closed-interval-ℚ p q r s H
+              ( is-positive-le-zero-ℚ s 0<s)))
+
+abstract
+  right-mul-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r →
+    is-in-unordered-closed-interval-ℚ (s *ℚ p) (s *ℚ q) (s *ℚ r)
+  right-mul-closed-interval-ℚ p q r s r∈[p,q] =
+    tr
+      ( is-in-unordered-closed-interval-ℚ (s *ℚ p) (s *ℚ q))
+      ( commutative-mul-ℚ r s)
+      ( binary-tr
+        ( λ a b → is-in-unordered-closed-interval-ℚ a b (r *ℚ s))
+        ( commutative-mul-ℚ p s)
+        ( commutative-mul-ℚ q s)
+        ( left-mul-closed-interval-ℚ p q r s r∈[p,q]))
+
+abstract
+  mul-closed-interval-closed-interval-ℚ :
+    (p q r s t u : ℚ) →
+    is-in-closed-interval-ℚ p q r →
+    is-in-closed-interval-ℚ s t u →
+    is-in-closed-interval-ℚ
+      (min-ℚ (min-ℚ (p *ℚ s) (p *ℚ t)) (min-ℚ (q *ℚ s) (q *ℚ t)))
+      (max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t)))
+      (r *ℚ u)
+  mul-closed-interval-closed-interval-ℚ p q r s t u r∈[p,q] u∈[s,t] =
+    let
+      (min-pu-qu≤ru , ru≤max-pu-qu) = left-mul-closed-interval-ℚ p q r u r∈[p,q]
+      (min-ps-pt≤pu , pu≤max-ps-pt) =
+        right-mul-closed-interval-ℚ s t u p u∈[s,t]
+      (min-qs-qt≤qu , qu≤max-qs-qt) =
+        right-mul-closed-interval-ℚ s t u q u∈[s,t]
+    in
+      transitive-leq-ℚ
+        ( min-ℚ (min-ℚ (p *ℚ s) (p *ℚ t)) (min-ℚ (q *ℚ s) (q *ℚ t)))
+        ( min-ℚ (p *ℚ u) (q *ℚ u))
+        ( r *ℚ u)
+        ( min-pu-qu≤ru)
+        ( min-leq-leq-ℚ
+          ( min-ℚ (p *ℚ s) (p *ℚ t))
+          ( p *ℚ u)
+          ( min-ℚ (q *ℚ s) (q *ℚ t))
+          ( q *ℚ u)
+          ( min-ps-pt≤pu)
+          ( min-qs-qt≤qu)) ,
+      transitive-leq-ℚ
+        ( r *ℚ u)
+        ( max-ℚ (p *ℚ u) (q *ℚ u))
+        ( max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t)))
+        ( max-leq-leq-ℚ
+          ( p *ℚ u)
+          ( max-ℚ (p *ℚ s) (p *ℚ t))
+          ( q *ℚ u)
+          ( max-ℚ (q *ℚ s) (q *ℚ t))
+          ( pu≤max-ps-pt)
+          ( qu≤max-qs-qt))
+        ( ru≤max-pu-qu)
+```
diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md
index e87b85c1c3..4da09c34b8 100644
--- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md
+++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md
@@ -24,6 +24,7 @@ open import elementary-number-theory.positive-integers
 open import elementary-number-theory.strict-inequality-integers
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
@@ -194,3 +195,18 @@ module _
             ( numerator-fraction-ℤ x)
             ( denominator-fraction-ℤ y))))
 ```
+
+### Negation reverses the order of inequality on integer fractions
+
+```agda
+neg-leq-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  leq-fraction-ℤ x y →
+  leq-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x)
+neg-leq-fraction-ℤ (m , n , p) (m' , n' , p') H =
+  binary-tr
+    ( leq-ℤ)
+    ( inv (left-negative-law-mul-ℤ m' n))
+    ( inv (left-negative-law-mul-ℤ m n'))
+    ( neg-leq-ℤ (m *ℤ n') (m' *ℤ n) H)
+```
diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
index 1e9c9063f6..cd0ac5c223 100644
--- a/src/elementary-number-theory/inequality-integers.lagda.md
+++ b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -285,6 +285,17 @@ module _
           ( I))
 ```
 
+### Negation of integers reverses inequality
+
+```agda
+neg-leq-ℤ : (x y : ℤ) → leq-ℤ x y → leq-ℤ (neg-ℤ y) (neg-ℤ x)
+neg-leq-ℤ x y =
+  tr
+    ( is-nonnegative-ℤ)
+    ( ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙
+      commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x))
+```
+
 ## See also
 
 - The decidable total order on the integers is defined in
diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
index e602ea684a..4d2603dade 100644
--- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
@@ -104,6 +104,9 @@ leq-ℚ-Decidable-Prop x y =
 refl-leq-ℚ : (x : ℚ) → leq-ℚ x x
 refl-leq-ℚ x =
   refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x)
+
+leq-eq-ℚ : (x y : ℚ) → x ＝ y → leq-ℚ x y
+leq-eq-ℚ x y x=y = tr (leq-ℚ x) x=y (refl-leq-ℚ x)
 ```
 
 ### Inequality on the rational numbers is antisymmetric
@@ -412,6 +415,13 @@ pr1 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-left-diff-ℚ x y z
 pr2 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-right-add-ℚ x z y
 ```
 
+### Negation of rational numbers reverses inequality
+
+```agda
+neg-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ (neg-ℚ y) (neg-ℚ x)
+neg-leq-ℚ x y = neg-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
+```
+
 ## See also
 
 - The decidable total order on the rational numbers is defined in
diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md
index 246ccf0e7c..3ee0891636 100644
--- a/src/elementary-number-theory/integer-fractions.lagda.md
+++ b/src/elementary-number-theory/integer-fractions.lagda.md
@@ -110,6 +110,14 @@ neg-fraction-ℤ (d , n) = (neg-ℤ d , n)
 
 ## Properties
 
+### The double negation of an integer fraction is the original fraction
+
+```agda
+abstract
+  neg-neg-fraction-ℤ : (x : fraction-ℤ) → neg-fraction-ℤ (neg-fraction-ℤ x) ＝ x
+  neg-neg-fraction-ℤ (n , d) = ap (_, d) (neg-neg-ℤ n)
+```
+
 ### Denominators are nonzero
 
 ```agda
diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md
index 59124d8e82..9bb3eab066 100644
--- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md
@@ -43,74 +43,84 @@ max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ### Associativity of the maximum operation
 
 ```agda
-associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z)
-associative-max-ℚ =
-  associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z)
+  associative-max-ℚ =
+    associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### Commutativity of the maximum operation
 
 ```agda
-commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x
-commutative-max-ℚ =
-  commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x
+  commutative-max-ℚ =
+    commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### The maximum operation is idempotent
 
 ```agda
-idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x
-idempotent-max-ℚ =
-  idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x
+  idempotent-max-ℚ =
+    idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### The maximum is an upper bound
 
 ```agda
-leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y
-leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y
+  leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 
-leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y
-leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+  leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y
+  leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### If `a` is less than or equal to `b`, then the maximum of `a` and `b` is `b`
 
 ```agda
-left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y
-left-leq-right-max-ℚ =
-  left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order
-
-right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x
-right-leq-left-max-ℚ =
-  right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y
+  left-leq-right-max-ℚ =
+    left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+
+  right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x
+  right-leq-left-max-ℚ =
+    right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### If both `x` and `y` are less than `z`, so is their maximum
 
 ```agda
-le-max-le-both-ℚ : (z x y : ℚ) → le-ℚ x z → le-ℚ y z → le-ℚ (max-ℚ x y) z
-le-max-le-both-ℚ z x y x<z y<z with decide-le-leq-ℚ x y
-... | inl x<y =
-  inv-tr
-    ( λ w → le-ℚ w z)
-    ( left-leq-right-max-Decidable-Total-Order
-      ( ℚ-Decidable-Total-Order)
-      ( x)
-      ( y)
-      ( leq-le-ℚ {x} {y} x<y))
-    ( y<z)
-... | inr y≤x =
-  inv-tr
-    ( λ w → le-ℚ w z)
-    ( right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order x y y≤x)
-    ( x<z)
+abstract
+  le-max-le-both-ℚ : (z x y : ℚ) → le-ℚ x z → le-ℚ y z → le-ℚ (max-ℚ x y) z
+  le-max-le-both-ℚ z x y x<z y<z with decide-le-leq-ℚ x y
+  ... | inl x<y =
+    inv-tr
+      ( λ w → le-ℚ w z)
+      ( left-leq-right-max-Decidable-Total-Order
+        ( ℚ-Decidable-Total-Order)
+        ( x)
+        ( y)
+        ( leq-le-ℚ {x} {y} x<y))
+      ( y<z)
+  ... | inr y≤x =
+    inv-tr
+      ( λ w → le-ℚ w z)
+      ( right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+        ( x)
+        ( y)
+        ( y≤x))
+      ( x<z)
 ```
 
 ### If `a ≤ b` and `c ≤ d`, then `max a c ≤ max b d`
 
 ```agda
-max-leq-leq-ℚ :
-  (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (max-ℚ a c) (max-ℚ b d)
-max-leq-leq-ℚ = max-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  max-leq-leq-ℚ :
+    (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (max-ℚ a c) (max-ℚ b d)
+  max-leq-leq-ℚ = max-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
diff --git a/src/elementary-number-theory/minimum-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-rational-numbers.lagda.md
index a0e9cf67da..434ce781ec 100644
--- a/src/elementary-number-theory/minimum-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/minimum-rational-numbers.lagda.md
@@ -44,74 +44,82 @@ min-ℚ = min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ### Associativity of the minimum operation
 
 ```agda
-associative-min-ℚ : (x y z : ℚ) → min-ℚ (min-ℚ x y) z ＝ min-ℚ x (min-ℚ y z)
-associative-min-ℚ =
-  associative-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  associative-min-ℚ : (x y z : ℚ) → min-ℚ (min-ℚ x y) z ＝ min-ℚ x (min-ℚ y z)
+  associative-min-ℚ =
+    associative-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### Commutativity of the minimum operation
 
 ```agda
-commutative-min-ℚ : (x y : ℚ) → min-ℚ x y ＝ min-ℚ y x
-commutative-min-ℚ =
-  commutative-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  commutative-min-ℚ : (x y : ℚ) → min-ℚ x y ＝ min-ℚ y x
+  commutative-min-ℚ =
+    commutative-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### The minimum operation is idempotent
 
 ```agda
-idempotent-min-ℚ : (x : ℚ) → min-ℚ x x ＝ x
-idempotent-min-ℚ =
-  idempotent-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  idempotent-min-ℚ : (x : ℚ) → min-ℚ x x ＝ x
+  idempotent-min-ℚ =
+    idempotent-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### The minimum is a lower bound
 
 ```agda
-leq-left-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ x
-leq-left-min-ℚ = leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  leq-left-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ x
+  leq-left-min-ℚ = leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 
-leq-right-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ y
-leq-right-min-ℚ = leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+  leq-right-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ y
+  leq-right-min-ℚ = leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### If `a` is less than or equal to `b`, then the minimum of `a` and `b` is `a`
 
 ```agda
-left-leq-right-min-ℚ : (x y : ℚ) → leq-ℚ x y → min-ℚ x y ＝ x
-left-leq-right-min-ℚ =
-  left-leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
-
-right-leq-left-min-ℚ : (x y : ℚ) → leq-ℚ y x → min-ℚ x y ＝ y
-right-leq-left-min-ℚ =
-  right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  left-leq-right-min-ℚ : (x y : ℚ) → leq-ℚ x y → min-ℚ x y ＝ x
+  left-leq-right-min-ℚ =
+    left-leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+
+  right-leq-left-min-ℚ : (x y : ℚ) → leq-ℚ y x → min-ℚ x y ＝ y
+  right-leq-left-min-ℚ =
+    right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
 
 ### If `z` is less than both `x` and `y`, it is less than their minimum
 
 ```agda
-le-min-le-both-ℚ : (z x y : ℚ) → le-ℚ z x → le-ℚ z y → le-ℚ z (min-ℚ x y)
-le-min-le-both-ℚ z x y z<x z<y with decide-le-leq-ℚ x y
-... | inl x<y =
-  inv-tr
-    ( le-ℚ z)
-    ( left-leq-right-min-Decidable-Total-Order
-      ( ℚ-Decidable-Total-Order)
-      ( x)
-      ( y)
-      ( leq-le-ℚ {x} {y} x<y))
-    ( z<x)
-... | inr y≤x =
-  inv-tr
-    ( le-ℚ z)
-    ( right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order x y y≤x)
-    ( z<y)
+abstract
+  le-min-le-both-ℚ : (z x y : ℚ) → le-ℚ z x → le-ℚ z y → le-ℚ z (min-ℚ x y)
+  le-min-le-both-ℚ z x y z<x z<y with decide-le-leq-ℚ x y
+  ... | inl x<y =
+    inv-tr
+      ( le-ℚ z)
+      ( left-leq-right-min-Decidable-Total-Order
+        ( ℚ-Decidable-Total-Order)
+        ( x)
+        ( y)
+        ( leq-le-ℚ {x} {y} x<y))
+      ( z<x)
+  ... | inr y≤x =
+    inv-tr
+      ( le-ℚ z)
+      ( right-leq-left-min-Decidable-Total-Order
+          ℚ-Decidable-Total-Order x y y≤x)
+      ( z<y)
 ```
 
 ### If `a ≤ b` and `c ≤ d`, then `min a c ≤ min b d`
 
 ```agda
-min-leq-leq-ℚ :
-  (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (min-ℚ a c) (min-ℚ b d)
-min-leq-leq-ℚ = min-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order
+abstract
+  min-leq-leq-ℚ :
+    (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (min-ℚ a c) (min-ℚ b d)
+  min-leq-leq-ℚ = min-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order
 ```
diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md
index a8c0e801c0..c2f96f0721 100644
--- a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md
+++ b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md
@@ -23,6 +23,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 ```
 
@@ -302,6 +303,35 @@ is-nonnegative-right-factor-mul-ℤ {x} {y} H =
     ( is-nonnegative-eq-ℤ (commutative-mul-ℤ x y) H)
 ```
 
+### The left factor of a negative product with a positive right factor is negative
+
+```agda
+abstract
+  is-negative-left-factor-mul-positive-ℤ :
+    {x y : ℤ} → is-negative-ℤ (x *ℤ y) → is-positive-ℤ y → is-negative-ℤ x
+  is-negative-left-factor-mul-positive-ℤ {inl x} {inr (inr y)} _ _ = star
+  is-negative-left-factor-mul-positive-ℤ {inr x} {inr (inr y)} H _ =
+    is-not-negative-and-nonnegative-ℤ
+      ( inr x *ℤ inr (inr y))
+      ( H ,
+        is-nonnegative-mul-nonnegative-positive-ℤ
+          { inr x}
+          { inr (inr y)}
+          ( star)
+          ( star))
+```
+
+### The right factor of a negative product with a positive right factor is negative
+
+```agda
+abstract
+  is-negative-right-factor-mul-positive-ℤ :
+    {x y : ℤ} → is-negative-ℤ (x *ℤ y) → is-positive-ℤ x → is-negative-ℤ y
+  is-negative-right-factor-mul-positive-ℤ {x} {y} xy-is-neg =
+    is-negative-left-factor-mul-positive-ℤ
+      ( tr is-negative-ℤ (commutative-mul-ℤ x y) xy-is-neg)
+```
+
 ## Definitions
 
 ### Multiplication by a signed integer
diff --git a/src/elementary-number-theory/negative-integer-fractions.lagda.md b/src/elementary-number-theory/negative-integer-fractions.lagda.md
new file mode 100644
index 0000000000..4b8de8ccd7
--- /dev/null
+++ b/src/elementary-number-theory/negative-integer-fractions.lagda.md
@@ -0,0 +1,139 @@
+# Negative integer fractions
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.negative-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-integer-fractions
+open import elementary-number-theory.addition-positive-and-negative-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.multiplication-positive-and-negative-integers
+open import elementary-number-theory.negative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integer-fractions
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.reduced-integer-fractions
+
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [integer fraction](elementary-number-theory.integer-fractions.md) `x` is said
+to be
+{{#concept "negative" Disambiguation="integer fraction" Agda=is-negative-fraction-ℤ}}
+if its numerator is a
+[negative integer](elementary-number-theory.negative-integers.md).
+
+## Definitions
+
+### The property of being a negative integer fraction
+
+```agda
+module _
+  (x : fraction-ℤ)
+  where
+
+  is-negative-fraction-ℤ : UU lzero
+  is-negative-fraction-ℤ = is-negative-ℤ (numerator-fraction-ℤ x)
+
+  is-prop-is-negative-fraction-ℤ : is-prop is-negative-fraction-ℤ
+  is-prop-is-negative-fraction-ℤ =
+    is-prop-is-negative-ℤ (numerator-fraction-ℤ x)
+```
+
+## Properties
+
+### The negative of a positive integer fraction is negative
+
+```agda
+abstract
+  is-negative-neg-positive-fraction-ℤ :
+    (x : fraction-ℤ) → is-positive-fraction-ℤ x →
+    is-negative-fraction-ℤ (neg-fraction-ℤ x)
+  is-negative-neg-positive-fraction-ℤ _ = is-negative-neg-is-positive-ℤ
+```
+
+### The negative of a negative integer fraction is positive
+
+```agda
+abstract
+  is-positive-neg-negative-fraction-ℤ :
+    (x : fraction-ℤ) → is-negative-fraction-ℤ x →
+    is-positive-fraction-ℤ (neg-fraction-ℤ x)
+  is-positive-neg-negative-fraction-ℤ _ = is-positive-neg-is-negative-ℤ
+```
+
+### An integer fraction similar to a negative integer fraction is negative
+
+```agda
+is-negative-sim-fraction-ℤ :
+  (x y : fraction-ℤ) (S : sim-fraction-ℤ x y) →
+  is-negative-fraction-ℤ x →
+  is-negative-fraction-ℤ y
+is-negative-sim-fraction-ℤ x y S N =
+  is-negative-right-factor-mul-positive-ℤ
+    ( is-negative-eq-ℤ
+      ( S ∙
+        commutative-mul-ℤ (numerator-fraction-ℤ y) (denominator-fraction-ℤ x))
+      ( is-negative-mul-negative-positive-ℤ
+        ( N)
+        ( is-positive-denominator-fraction-ℤ y)))
+    ( is-positive-denominator-fraction-ℤ x)
+```
+
+### The reduced fraction of a negative integer fraction is negative
+
+```agda
+is-negative-reduce-fraction-ℤ :
+  {x : fraction-ℤ} (P : is-negative-fraction-ℤ x) →
+  is-negative-fraction-ℤ (reduce-fraction-ℤ x)
+is-negative-reduce-fraction-ℤ {x} =
+  is-negative-sim-fraction-ℤ
+    ( x)
+    ( reduce-fraction-ℤ x)
+    ( sim-reduced-fraction-ℤ x)
+```
+
+### The sum of two negative integer fractions is negative
+
+```agda
+is-negative-add-fraction-ℤ :
+  {x y : fraction-ℤ} →
+  is-negative-fraction-ℤ x →
+  is-negative-fraction-ℤ y →
+  is-negative-fraction-ℤ (add-fraction-ℤ x y)
+is-negative-add-fraction-ℤ {x} {y} P Q =
+  is-negative-add-ℤ
+    ( is-negative-mul-negative-positive-ℤ
+      ( P)
+      ( is-positive-denominator-fraction-ℤ y))
+    ( is-negative-mul-negative-positive-ℤ
+      ( Q)
+      ( is-positive-denominator-fraction-ℤ x))
+```
+
+### The product of two negative integer fractions is positive
+
+```agda
+is-positive-mul-negative-fraction-ℤ :
+  {x y : fraction-ℤ} →
+  is-negative-fraction-ℤ x →
+  is-negative-fraction-ℤ y →
+  is-positive-fraction-ℤ (mul-fraction-ℤ x y)
+is-positive-mul-negative-fraction-ℤ = is-positive-mul-negative-ℤ
+```
diff --git a/src/elementary-number-theory/negative-rational-numbers.lagda.md b/src/elementary-number-theory/negative-rational-numbers.lagda.md
new file mode 100644
index 0000000000..509bde6870
--- /dev/null
+++ b/src/elementary-number-theory/negative-rational-numbers.lagda.md
@@ -0,0 +1,272 @@
+# Negative rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.negative-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.difference-rational-numbers
+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.multiplication-rational-numbers
+open import elementary-number-theory.negative-integer-fractions
+open import elementary-number-theory.negative-integers
+open import elementary-number-theory.nonzero-rational-numbers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integer-fractions
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [rational number](elementary-number-theory.rational-numbers.md) `x` is said to
+be {{#concept "negative" Disambiguation="rational number" Agda=is-negative-ℚ}}
+if its negation is positive.
+
+Negative rational numbers are a [subsemigroup](group-theory.subsemigroups.md) of
+the
+[additive monoid of rational numbers](elementary-number-theory.additive-group-of-rational-numbers.md).
+
+## Definitions
+
+### The property of being a negative rational number
+
+```agda
+module _
+  (q : ℚ)
+  where
+
+  is-negative-ℚ : UU lzero
+  is-negative-ℚ = is-positive-ℚ (neg-ℚ q)
+
+  is-prop-is-negative-ℚ : is-prop is-negative-ℚ
+  is-prop-is-negative-ℚ = is-prop-is-positive-ℚ (neg-ℚ q)
+
+  is-negative-prop-ℚ : Prop lzero
+  pr1 is-negative-prop-ℚ = is-negative-ℚ
+  pr2 is-negative-prop-ℚ = is-prop-is-negative-ℚ
+```
+
+### The type of negative rational numbers
+
+```agda
+negative-ℚ : UU lzero
+negative-ℚ = type-subtype is-negative-prop-ℚ
+
+ℚ⁻ : UU lzero
+ℚ⁻ = negative-ℚ
+
+module _
+  (x : negative-ℚ)
+  where
+
+  rational-ℚ⁻ : ℚ
+  rational-ℚ⁻ = pr1 x
+
+  fraction-ℚ⁻ : fraction-ℤ
+  fraction-ℚ⁻ = fraction-ℚ rational-ℚ⁻
+
+  numerator-ℚ⁻ : ℤ
+  numerator-ℚ⁻ = numerator-ℚ rational-ℚ⁻
+
+  denominator-ℚ⁻ : ℤ
+  denominator-ℚ⁻ = denominator-ℚ rational-ℚ⁻
+
+  is-negative-rational-ℚ⁻ : is-negative-ℚ rational-ℚ⁻
+  is-negative-rational-ℚ⁻ = pr2 x
+
+  is-negative-fraction-ℚ⁻ : is-negative-fraction-ℤ fraction-ℚ⁻
+  is-negative-fraction-ℚ⁻ =
+    tr
+      ( is-negative-fraction-ℤ)
+      ( neg-neg-fraction-ℤ fraction-ℚ⁻)
+      ( is-negative-neg-positive-fraction-ℤ
+        ( neg-fraction-ℤ fraction-ℚ⁻)
+        ( is-negative-rational-ℚ⁻))
+
+  is-negative-numerator-ℚ⁻ : is-negative-ℤ numerator-ℚ⁻
+  is-negative-numerator-ℚ⁻ = is-negative-fraction-ℚ⁻
+
+  is-positive-denominator-ℚ⁻ : is-positive-ℤ denominator-ℚ⁻
+  is-positive-denominator-ℚ⁻ = is-positive-denominator-ℚ rational-ℚ⁻
+
+  neg-ℚ⁻ : ℚ⁺
+  neg-ℚ⁻ = (neg-ℚ rational-ℚ⁻) , is-negative-rational-ℚ⁻
+
+neg-ℚ⁺ : ℚ⁺ → ℚ⁻
+neg-ℚ⁺ (q , q-is-pos) = neg-ℚ q , inv-tr is-positive-ℚ (neg-neg-ℚ q) q-is-pos
+
+abstract
+  eq-ℚ⁻ : {x y : ℚ⁻} → rational-ℚ⁻ x ＝ rational-ℚ⁻ y → x ＝ y
+  eq-ℚ⁻ {x} {y} = eq-type-subtype is-negative-prop-ℚ
+```
+
+## Properties
+
+### The negative rational numbers form a set
+
+```agda
+is-set-ℚ⁻ : is-set ℚ⁻
+is-set-ℚ⁻ = is-set-type-subtype is-negative-prop-ℚ is-set-ℚ
+```
+
+### The rational image of a negative integer is negative
+
+```agda
+abstract
+  is-negative-rational-ℤ :
+    (x : ℤ) → is-negative-ℤ x → is-negative-ℚ (rational-ℤ x)
+  is-negative-rational-ℤ _ = is-positive-neg-is-negative-ℤ
+
+negative-rational-negative-ℤ : negative-ℤ → ℚ⁻
+negative-rational-negative-ℤ (x , x-is-neg) =
+  rational-ℤ x , is-negative-rational-ℤ x x-is-neg
+```
+
+### The rational image of a negative integer fraction is negative
+
+```agda
+abstract
+  is-negative-rational-fraction-ℤ :
+    {x : fraction-ℤ} (P : is-negative-fraction-ℤ x) →
+    is-negative-ℚ (rational-fraction-ℤ x)
+  is-negative-rational-fraction-ℤ P =
+    is-positive-neg-is-negative-ℤ (is-negative-reduce-fraction-ℤ P)
+```
+
+### A rational number `x` is negative if and only if `x < 0`
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  abstract
+    le-zero-is-negative-ℚ : is-negative-ℚ x → le-ℚ x zero-ℚ
+    le-zero-is-negative-ℚ x-is-neg =
+      tr
+        ( λ y → le-ℚ y zero-ℚ)
+        ( neg-neg-ℚ x)
+        ( neg-le-ℚ zero-ℚ (neg-ℚ x) (le-zero-is-positive-ℚ (neg-ℚ x) x-is-neg))
+
+    is-negative-le-zero-ℚ : le-ℚ x zero-ℚ → is-negative-ℚ x
+    is-negative-le-zero-ℚ x-is-neg =
+      is-positive-le-zero-ℚ (neg-ℚ x) (neg-le-ℚ x zero-ℚ x-is-neg)
+
+    is-negative-iff-le-zero-ℚ : is-negative-ℚ x ↔ le-ℚ x zero-ℚ
+    is-negative-iff-le-zero-ℚ =
+      le-zero-is-negative-ℚ ,
+      is-negative-le-zero-ℚ
+```
+
+### The difference of a rational number with a greater rational number is negative
+
+```agda
+module _
+  (x y : ℚ) (H : le-ℚ x y)
+  where
+
+  abstract
+    is-negative-diff-le-ℚ : is-negative-ℚ (x -ℚ y)
+    is-negative-diff-le-ℚ =
+      inv-tr
+        ( is-positive-ℚ)
+        ( distributive-neg-diff-ℚ x y)
+        ( is-positive-diff-le-ℚ x y H)
+
+  negative-diff-le-ℚ : ℚ⁻
+  negative-diff-le-ℚ = x -ℚ y , is-negative-diff-le-ℚ
+```
+
+### Negative rational numbers are nonzero
+
+```agda
+abstract
+  is-nonzero-is-negative-ℚ : {x : ℚ} → is-negative-ℚ x → is-nonzero-ℚ x
+  is-nonzero-is-negative-ℚ {x} H =
+    tr
+      ( is-nonzero-ℚ)
+      ( neg-neg-ℚ x)
+      ( is-nonzero-neg-ℚ (is-nonzero-is-positive-ℚ H))
+```
+
+### The product of two negative rational numbers is positive
+
+```agda
+abstract
+  is-positive-mul-negative-ℚ :
+    {x y : ℚ} → is-negative-ℚ x → is-negative-ℚ y → is-positive-ℚ (x *ℚ y)
+  is-positive-mul-negative-ℚ {x} {y} P Q =
+    is-positive-reduce-fraction-ℤ
+      ( is-positive-mul-negative-fraction-ℤ
+        { fraction-ℚ x}
+        { fraction-ℚ y}
+        ( is-negative-fraction-ℚ⁻ (x , P))
+        ( is-negative-fraction-ℚ⁻ (y , Q)))
+```
+
+### Multiplication by a negative rational number reverses inequality
+
+```agda
+module _
+  (p : ℚ⁻)
+  (q r : ℚ)
+  (H : leq-ℚ q r)
+  where
+
+  abstract
+    reverses-leq-right-mul-ℚ⁻ : leq-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p)
+    reverses-leq-right-mul-ℚ⁻ =
+      binary-tr
+        ( leq-ℚ)
+        ( negative-law-mul-ℚ r (rational-ℚ⁻ p))
+        ( negative-law-mul-ℚ q (rational-ℚ⁻ p))
+        ( preserves-leq-right-mul-ℚ⁺
+          ( neg-ℚ⁻ p)
+          ( neg-ℚ r)
+          ( neg-ℚ q)
+          ( neg-leq-ℚ q r H))
+```
+
+### Multiplication by a negative rational number reverses strict inequality
+
+```agda
+module _
+  (p : ℚ⁻)
+  (q r : ℚ)
+  (H : le-ℚ q r)
+  where
+
+  abstract
+    reverses-le-right-mul-ℚ⁻ : le-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p)
+    reverses-le-right-mul-ℚ⁻ =
+      binary-tr
+        ( le-ℚ)
+        ( negative-law-mul-ℚ r (rational-ℚ⁻ p))
+        ( negative-law-mul-ℚ q (rational-ℚ⁻ p))
+        ( preserves-le-right-mul-ℚ⁺
+          ( neg-ℚ⁻ p)
+          ( neg-ℚ r)
+          ( neg-ℚ q)
+          ( neg-le-ℚ q r H))
+```
diff --git a/src/elementary-number-theory/positive-and-negative-integers.lagda.md b/src/elementary-number-theory/positive-and-negative-integers.lagda.md
index 844b95a8b8..9f35831163 100644
--- a/src/elementary-number-theory/positive-and-negative-integers.lagda.md
+++ b/src/elementary-number-theory/positive-and-negative-integers.lagda.md
@@ -51,6 +51,15 @@ is-not-negative-and-positive-ℤ (inl x) (H , K) = K
 is-not-negative-and-positive-ℤ (inr x) (H , K) = H
 ```
 
+### No integer is both nonnegative and negative
+
+```agda
+is-not-negative-and-nonnegative-ℤ :
+  (x : ℤ) → ¬ (is-negative-ℤ x × is-nonnegative-ℤ x)
+is-not-negative-and-nonnegative-ℤ (inl x) (H , K) = K
+is-not-negative-and-nonnegative-ℤ (inr x) (H , K) = H
+```
+
 ### Dichotomies
 
 #### A nonzero integer is either negative or positive
diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md
index a30df38014..04f5c23411 100644
--- a/src/elementary-number-theory/positive-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md
@@ -14,6 +14,7 @@ open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.additive-group-of-rational-numbers
 open import elementary-number-theory.cross-multiplication-difference-integer-fractions
 open import elementary-number-theory.difference-rational-numbers
+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
@@ -160,15 +161,14 @@ positive-rational-positive-ℤ : positive-ℤ → ℚ⁺
 positive-rational-positive-ℤ (z , pos-z) = rational-ℤ z , pos-z
 
 one-ℚ⁺ : ℚ⁺
-one-ℚ⁺ = positive-rational-positive-ℤ one-positive-ℤ
+one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ)
 ```
 
-### Embedding of nonzero natural numbers in the positive rational numbers
+### The rational image of a positive natural number is positive
 
 ```agda
 positive-rational-ℕ⁺ : ℕ⁺ → ℚ⁺
-positive-rational-ℕ⁺ n =
-  positive-rational-positive-ℤ (positive-int-ℕ⁺ n)
+positive-rational-ℕ⁺ n = positive-rational-positive-ℤ (positive-int-ℕ⁺ n)
 ```
 
 ### The rational image of a positive integer fraction is positive
@@ -587,6 +587,42 @@ preserves-le-right-mul-ℚ⁺ p⁺@(p , _) q r q<r =
     ( preserves-le-left-mul-ℚ⁺ p⁺ q r q<r)
 ```
 
+### Multiplication by a positive rational number preserves inequality
+
+```agda
+preserves-leq-left-mul-ℚ⁺ :
+  (p : ℚ⁺) (q r : ℚ) → leq-ℚ q r →
+  leq-ℚ (rational-ℚ⁺ p *ℚ q) (rational-ℚ⁺ p *ℚ r)
+preserves-leq-left-mul-ℚ⁺
+  p⁺@((p@(p-num , p-denom , p-denom-pos) , _) , p-num-pos)
+  q@((q-num , q-denom , _) , _)
+  r@((r-num , r-denom , _) , _)
+  q≤r =
+    preserves-leq-rational-fraction-ℤ
+      ( mul-fraction-ℤ p (fraction-ℚ q))
+      ( mul-fraction-ℤ p (fraction-ℚ r))
+      ( binary-tr
+        ( leq-ℤ)
+        ( interchange-law-mul-mul-ℤ _ _ _ _)
+        ( interchange-law-mul-mul-ℤ _ _ _ _)
+        ( preserves-leq-right-mul-nonnegative-ℤ
+          ( nonnegative-positive-ℤ
+            ( mul-positive-ℤ (p-num , p-num-pos) (p-denom , p-denom-pos)))
+          ( q-num *ℤ r-denom)
+          ( r-num *ℤ q-denom)
+          ( q≤r)))
+
+preserves-leq-right-mul-ℚ⁺ :
+  (p : ℚ⁺) (q r : ℚ) → leq-ℚ q r →
+  leq-ℚ (q *ℚ rational-ℚ⁺ p) (r *ℚ rational-ℚ⁺ p)
+preserves-leq-right-mul-ℚ⁺ p q r q≤r =
+  binary-tr
+    ( leq-ℚ)
+    ( commutative-mul-ℚ (rational-ℚ⁺ p) q)
+    ( commutative-mul-ℚ (rational-ℚ⁺ p) r)
+    ( preserves-leq-left-mul-ℚ⁺ p q r q≤r)
+```
+
 ### Multiplication of a positive rational by another positive rational less than 1 is a strictly deflationary map
 
 ```agda