Refactoring positive integers

src/elementary-number-theory.lagda.md

@@ -92,13 +92,18 @@ 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-integers 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
 open import elementary-number-theory.nonzero-natural-numbers public
 open import elementary-number-theory.ordinal-induction-natural-numbers public
 open import elementary-number-theory.parity-natural-numbers public
 open import elementary-number-theory.peano-arithmetic public
 open import elementary-number-theory.pisano-periods public
 open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public
+open import elementary-number-theory.positive-and-negative-integers public
+open import elementary-number-theory.positive-integers public
 open import elementary-number-theory.powers-integers public
 open import elementary-number-theory.powers-of-two public
 open import elementary-number-theory.prime-numbers public

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -14,6 +14,8 @@ open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types

src/elementary-number-theory/addition-integers.lagda.md

@@ -10,6 +10,9 @@ module elementary-number-theory.addition-integers where
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.integers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
@@ -23,6 +26,7 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.interchange-law
+open import foundation.transport-along-identifications
 open import foundation.unit-type
 ```
 
@@ -516,12 +520,12 @@ is-nonnegative-add-ℤ (inr (inl star)) (inr (inl star)) p q = star
 is-nonnegative-add-ℤ (inr (inl star)) (inr (inr n)) p q = star
 is-nonnegative-add-ℤ (inr (inr zero-ℕ)) (inr (inl star)) p q = star
 is-nonnegative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inl star)) star star =
-  is-nonnegative-succ-ℤ
+  is-nonnegative-succ-is-nonnegative-ℤ
     ( (inr (inr n)) +ℤ (inr (inl star)))
     ( is-nonnegative-add-ℤ (inr (inr n)) (inr (inl star)) star star)
 is-nonnegative-add-ℤ (inr (inr zero-ℕ)) (inr (inr m)) star star = star
 is-nonnegative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inr m)) star star =
-  is-nonnegative-succ-ℤ
+  is-nonnegative-succ-is-nonnegative-ℤ
     ( (inr (inr n)) +ℤ (inr (inr m)))
     ( is-nonnegative-add-ℤ (inr (inr n)) (inr (inr m)) star star)
 ```
@@ -533,9 +537,9 @@ is-positive-add-ℤ :
   {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y)
 is-positive-add-ℤ {inr (inr zero-ℕ)} {inr (inr y)} H K = star
 is-positive-add-ℤ {inr (inr (succ-ℕ x))} {inr (inr y)} H K =
-  is-positive-succ-ℤ
-    ( is-nonnegative-is-positive-ℤ
-      ( is-positive-add-ℤ {inr (inr x)} {inr (inr y)} star star))
+  is-positive-succ-is-positive-ℤ
+    ( add-ℤ (inr (inr x)) (inr (inr y)))
+    ( is-positive-add-ℤ {inr (inr x)} {inr (inr y)} H K)
 
 is-positive-add-nonnegative-positive-ℤ :
   {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y)

src/elementary-number-theory/bezouts-lemma-integers.lagda.md

@@ -22,6 +22,9 @@ open import elementary-number-theory.integers
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
@@ -194,25 +197,26 @@ bezouts-lemma-refactor-hypotheses x y H K =
   x-product-nonneg :
     is-nonnegative-ℤ
       ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ x)
-  x-product-nonneg = is-nonnegative-mul-ℤ
-    (is-nonnegative-int-ℕ
-      ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P))
-    (is-nonnegative-is-positive-ℤ H)
+  x-product-nonneg =
+    is-nonnegative-mul-ℤ
+      ( is-nonnegative-int-ℕ
+        ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P))
+      ( is-nonnegative-is-positive-ℤ x H)
   y-product-nonneg :
     is-nonnegative-ℤ
       ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ y)
   y-product-nonneg =
     is-nonnegative-mul-ℤ
       ( is-nonnegative-int-ℕ
         ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P))
-      ( is-nonnegative-is-positive-ℤ K)
+      ( is-nonnegative-is-positive-ℤ y K)
 
 bezouts-lemma-pos-ints :
   (x y : ℤ) (H : is-positive-ℤ x) (K : is-positive-ℤ y) →
   Σ ℤ (λ s → Σ ℤ (λ t → (s *ℤ x) +ℤ (t *ℤ y) ＝ gcd-ℤ x y))
 bezouts-lemma-pos-ints x y H K =
   sx-ty-nonneg-case-split
-    ( decide-is-nonnegative-ℤ {(s *ℤ x) -ℤ (t *ℤ y)})
+    ( decide-is-nonnegative-is-nonnegative-neg-ℤ {(s *ℤ x) -ℤ (t *ℤ y)})
   where
   s : ℤ
   s = int-ℕ (minimal-positive-distance-x-coeff

src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md

@@ -26,6 +26,8 @@ open import elementary-number-theory.modular-arithmetic
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
 open import elementary-number-theory.strict-inequality-natural-numbers
 open import elementary-number-theory.well-ordering-principle-natural-numbers
 
@@ -311,7 +313,7 @@ is-distance-between-multiples-div-mod-ℕ :
   (x y z : ℕ) →
   div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z) → is-distance-between-multiples-ℕ x y z
 is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) =
-  u-nonneg-case-split (decide-is-nonnegative-ℤ {u})
+  u-nonneg-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ {u})
   where
   u-nonneg-case-split :
     (is-nonnegative-ℤ u + is-nonnegative-ℤ (neg-ℤ u)) →
@@ -339,7 +341,7 @@ is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) =
               ( is-nonnegative-mul-ℤ neg (is-nonnegative-int-ℕ y))))))
 
 is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
-  uy-z-case-split (decide-is-nonnegative-ℤ
+  uy-z-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ
     { ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z))})
   where
   a : ℤ
@@ -714,31 +716,38 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
         ＝ z by abs-int-ℕ z))
     where
     neg-a-is-nonnegative-ℤ : is-nonnegative-ℤ (neg-ℤ a)
-    neg-a-is-nonnegative-ℤ = (is-nonnegative-left-factor-mul-ℤ
-      (tr is-nonnegative-ℤ
-      (equational-reasoning
-        neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ (int-ℕ z)))
-        ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
-          (neg-ℤ (neg-ℤ (int-ℕ z)))
-        by (distributive-neg-add-ℤ
-          ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          (neg-ℤ (int-ℕ z)))
-        ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
-          (int-ℕ z)
-        by ap ((neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_)
-          (neg-neg-ℤ (int-ℕ z))
-        ＝ add-ℤ (int-ℕ z)
-          (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-        by commutative-add-ℤ
-          (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-          (int-ℕ z)
-        ＝ (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))
-        by inv (pr2
-          (symmetric-cong-ℤ (int-ℕ (succ-ℕ x))
-            ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z)
-            (cong-div-mod-ℤ (succ-ℕ x) y z (u , p)))))
-        z-uy) (is-nonnegative-int-ℕ (succ-ℕ x)))
+    neg-a-is-nonnegative-ℤ =
+      is-nonnegative-left-factor-mul-ℤ
+        ( tr is-nonnegative-ℤ
+          ( equational-reasoning
+            ( neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ
+              ( neg-ℤ (int-ℕ z))))
+            ＝ ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
+                ( neg-ℤ (neg-ℤ (int-ℕ z)))
+              by
+                ( distributive-neg-add-ℤ
+                  ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
+                  ( neg-ℤ (int-ℕ z)))
+            ＝ ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
+                ( int-ℕ z)
+              by
+                ap
+                  ( (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_)
+                  ( neg-neg-ℤ (int-ℕ z))
+            ＝ add-ℤ
+              ( int-ℕ z)
+              ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
+              by
+                commutative-add-ℤ
+                  ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
+                  ( int-ℕ z)
+            ＝ (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))
+              by inv (pr2
+                ( symmetric-cong-ℤ (int-ℕ (succ-ℕ x))
+                ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z)
+                ( cong-div-mod-ℤ (succ-ℕ x) y z (u , p)))))
+          ( z-uy))
+          ( is-nonnegative-int-ℕ (succ-ℕ x))
 ```
 
 ### The type `is-distance-between-multiples-ℕ x y z` is decidable

src/elementary-number-theory/distance-integers.lagda.md

@@ -12,6 +12,9 @@ open import elementary-number-theory.difference-integers
 open import elementary-number-theory.distance-natural-numbers
 open import elementary-number-theory.integers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions

src/elementary-number-theory/divisibility-integers.lagda.md

@@ -14,7 +14,10 @@ open import elementary-number-theory.equality-integers
 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.nonzero-integers
+open import elementary-number-theory.positive-and-negative-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
@@ -657,23 +660,21 @@ is-plus-or-minus-sim-unit-ℤ {x} {y} H | inr nz | inr p =
 ```agda
 eq-sim-unit-is-nonnegative-ℤ :
   {a b : ℤ} → is-nonnegative-ℤ a → is-nonnegative-ℤ b → sim-unit-ℤ a b → a ＝ b
-eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K
-  with is-plus-or-minus-sim-unit-ℤ K
-eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inl pos = pos
-eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg
-  with is-decidable-is-zero-ℤ a
-eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inl z =
-  equational-reasoning
-    a
-    ＝ zero-ℤ
-      by z
-    ＝ neg-ℤ a
-      by inv (ap neg-ℤ z)
-    ＝ b
-      by neg
-eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inr nz =
-  ex-falso
-    ( nz
-      ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ
-          a H (tr is-nonnegative-ℤ (inv neg) H')))
+eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K with is-plus-or-minus-sim-unit-ℤ K
+...| inl p = p
+...| inr m = α ∙ inv β
+  where
+    α : is-zero-ℤ a
+    α =
+      is-zero-is-nonnegative-is-nonpositive-ℤ a H
+        ( is-nonpositive-eq-ℤ
+          ( inv (ap neg-ℤ m) ∙ (neg-neg-ℤ a))
+          ( is-nonpositive-neg-is-nonnegative-ℤ b H'))
+
+    β : is-zero-ℤ b
+    β =
+      is-zero-is-nonnegative-is-nonpositive-ℤ b H'
+        ( is-nonpositive-eq-ℤ
+          ( m)
+          ( is-nonpositive-neg-is-nonnegative-ℤ a H))
 ```

src/elementary-number-theory/greatest-common-divisor-integers.lagda.md

@@ -14,6 +14,9 @@ open import elementary-number-theory.equality-integers
 open import elementary-number-theory.greatest-common-divisor-natural-numbers
 open import elementary-number-theory.integers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
@@ -234,7 +237,7 @@ div-gcd-is-common-divisor-ℤ x y k H =
 is-positive-gcd-is-positive-left-ℤ :
   (x y : ℤ) → is-positive-ℤ x → is-positive-ℤ (gcd-ℤ x y)
 is-positive-gcd-is-positive-left-ℤ x y H =
-  is-positive-int-ℕ
+  is-positive-int-is-nonzero-ℕ
     ( gcd-ℕ (abs-ℤ x) (abs-ℤ y))
     ( is-nonzero-gcd-ℕ
       ( abs-ℤ x)
@@ -247,7 +250,7 @@ is-positive-gcd-is-positive-left-ℤ x y H =
 is-positive-gcd-is-positive-right-ℤ :
   (x y : ℤ) → is-positive-ℤ y → is-positive-ℤ (gcd-ℤ x y)
 is-positive-gcd-is-positive-right-ℤ x y H =
-  is-positive-int-ℕ
+  is-positive-int-is-nonzero-ℕ
     ( gcd-ℕ (abs-ℤ x) (abs-ℤ y))
     ( is-nonzero-gcd-ℕ
       ( abs-ℤ x)

src/elementary-number-theory/inequality-integer-fractions.lagda.md

@@ -15,6 +15,10 @@ open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.mediant-integer-fractions
 open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.nonpositive-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integers
 
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
@@ -80,11 +84,14 @@ module _
     sim-fraction-ℤ x y
   is-sim-antisymmetric-leq-fraction-ℤ H H' =
     sim-is-zero-coss-mul-diff-fraction-ℤ x y
-      ( is-zero-is-nonnegative-ℤ
+      ( is-zero-is-nonnegative-is-nonpositive-ℤ
+        ( cross-mul-diff-fraction-ℤ x y)
         ( H)
-        ( is-nonnegative-eq-ℤ
-            ( inv ( skew-commutative-cross-mul-diff-fraction-ℤ x y))
-            ( H')))
+        ( is-nonpositive-eq-ℤ
+          ( skew-commutative-cross-mul-diff-fraction-ℤ y x)
+          ( is-nonpositive-neg-is-nonnegative-ℤ
+            ( cross-mul-diff-fraction-ℤ y x)
+            ( H'))))
 ```
 
 ### Strict inequality on integer fractions is asymmetric
@@ -123,10 +130,12 @@ transitive-leq-fraction-ℤ p q r H H' =
           ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q)
           ( is-nonnegative-mul-ℤ
             ( is-nonnegative-is-positive-ℤ
+              ( denominator-fraction-ℤ p)
               ( is-positive-denominator-fraction-ℤ p))
             ( H'))
           ( is-nonnegative-mul-ℤ
             ( is-nonnegative-is-positive-ℤ
+              ( denominator-fraction-ℤ r)
               ( is-positive-denominator-fraction-ℤ r))
             ( H))))
     ( is-positive-denominator-fraction-ℤ q)
@@ -172,6 +181,7 @@ module _
         ( is-positive-add-nonnegative-positive-ℤ
           ( is-nonnegative-mul-ℤ
             ( is-nonnegative-is-positive-ℤ
+              ( denominator-fraction-ℤ p)
               ( is-positive-denominator-fraction-ℤ p))
             ( H'))
           ( is-positive-mul-ℤ
@@ -193,6 +203,7 @@ module _
             ( H'))
           ( is-nonnegative-mul-ℤ
             ( is-nonnegative-is-positive-ℤ
+              ( denominator-fraction-ℤ r)
               ( is-positive-denominator-fraction-ℤ r))
             ( H))))
       ( is-positive-denominator-fraction-ℤ q)
@@ -214,7 +225,8 @@ module _
       ( is-positive-eq-ℤ
         ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H)
         ( is-positive-mul-ℤ
-          ( is-positive-denominator-fraction-ℤ p) H'))
+          ( is-positive-denominator-fraction-ℤ p)
+          ( H')))
       ( is-positive-denominator-fraction-ℤ q)
 
   concatenate-le-sim-fraction-ℤ :
@@ -225,7 +237,9 @@ module _
     is-positive-right-factor-mul-ℤ
       ( is-positive-eq-ℤ
         ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H'))
-        ( is-positive-mul-ℤ (is-positive-denominator-fraction-ℤ r) H))
+        ( is-positive-mul-ℤ
+          ( is-positive-denominator-fraction-ℤ r)
+          ( H)))
       ( is-positive-denominator-fraction-ℤ q)
 ```