From fb4dd23a6e5ffd541c246fb34d3e7fd56ae13005 Mon Sep 17 00:00:00 2001
From: Louis Wasserman <wasserman.louis@gmail.com>
Date: Tue, 4 Feb 2025 08:38:03 -0800
Subject: [PATCH] =?UTF-8?q?Archimedean=20property=20of=20`fraction-?=
 =?UTF-8?q?=E2=84=A4`=20(#1261)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/elementary-number-theory.lagda.md         |  1 +
 ...medean-property-integer-fractions.lagda.md | 63 +++++++++++++++++++
 2 files changed, 64 insertions(+)
 create mode 100644 src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md

diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index d341a666f0..41595a97ba 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -17,6 +17,7 @@ open import elementary-number-theory.addition-natural-numbers public
 open import elementary-number-theory.addition-positive-and-negative-integers public
 open import elementary-number-theory.addition-rational-numbers public
 open import elementary-number-theory.additive-group-of-rational-numbers public
+open import elementary-number-theory.archimedean-property-integer-fractions public
 open import elementary-number-theory.archimedean-property-integers public
 open import elementary-number-theory.archimedean-property-natural-numbers public
 open import elementary-number-theory.arithmetic-functions public
diff --git a/src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md b/src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md
new file mode 100644
index 0000000000..1d20da58d6
--- /dev/null
+++ b/src/elementary-number-theory/archimedean-property-integer-fractions.lagda.md
@@ -0,0 +1,63 @@
+# The Archimedean property of integer fractions
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.archimedean-property-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.archimedean-property-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.natural-numbers
+open import elementary-number-theory.positive-integer-fractions
+open import elementary-number-theory.strict-inequality-integer-fractions
+open import elementary-number-theory.strict-inequality-integers
+
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+```
+
+</details>
+
+## Definition
+
+The Archimedean property of the integer fractions is that for any
+`x y : fraction-ℤ`, with positive `x`, there is an `n : ℕ` such that `y` is less
+than `n` as an integer fraction times `x`.
+
+```agda
+abstract
+  archimedean-property-fraction-ℤ :
+    (x y : fraction-ℤ) →
+    is-positive-fraction-ℤ x →
+    exists
+      ℕ
+      (λ n → le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x))
+  archimedean-property-fraction-ℤ
+    x@(px , qx , pos-qx) y@(py , qy , pos-qy) pos-px =
+      elim-exists
+        (∃
+          ( ℕ)
+          ( λ n →
+            le-fraction-ℤ-Prop y (in-fraction-ℤ (int-ℕ n) *fraction-ℤ x)))
+        ( λ n H →
+          intro-exists
+            ( n)
+            ( tr
+              ( le-ℤ (py *ℤ qx))
+              ( inv (associative-mul-ℤ (int-ℕ n) px qy))
+              ( H)))
+        ( archimedean-property-ℤ
+          ( px *ℤ qy)
+          ( py *ℤ qx)
+          ( is-positive-mul-ℤ pos-px pos-qy))
+```