Archimedean property of fraction-ℤ (#1261)

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

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))
+```