rename and clean

UniMath · Mar 7, 2024 · ad138be · ad138be
1 parent 8dd492a
commit ad138be
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 12 deletions.
diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
@@ -216,7 +216,7 @@ bezouts-lemma-pos-ints :
   Σ ℤ (λ 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

diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -313,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)) →
@@ -341,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 : ℤ

diff --git a/src/elementary-number-theory/positive-and-negative-integers.lagda.md b/src/elementary-number-theory/positive-and-negative-integers.lagda.md
@@ -46,14 +46,34 @@ integers
 
 ## Properties
 
-### The only nonnegative and nonpositive integer is `zero-ℤ`
+### Characterisations of `zero-ℤ`
+
+#### The only nonnegative and nonpositive integer is `zero-ℤ`
 
 ```agda
 is-zero-is-nonnegative-is-nonpositive-ℤ :
   (x : ℤ) → is-nonnegative-ℤ x → is-nonpositive-ℤ x → is-zero-ℤ x
 is-zero-is-nonnegative-is-nonpositive-ℤ (inr (inl x)) H K = refl
 ```
 
+#### The only nonnegative integer with a nonnegative negative is `zero-ℤ`
+
+```agda
+is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
+  (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x
+is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos =
+  refl
+```
+
+#### The only nonpositive integer with a nonpositive negative is zero-ℤ
+
+```agda
+is-zero-is-nonpositive-neg-is-nonpositive-ℤ :
+  (x : ℤ) → is-nonpositive-ℤ x → is-nonpositive-ℤ (neg-ℤ x) → is-zero-ℤ x
+is-zero-is-nonpositive-neg-is-nonpositive-ℤ (inr (inl star)) nonneg nonpos =
+  refl
+```
+
 ### Dichotomy properties
 
 #### A nonzero integer is either negative or positive
@@ -85,18 +105,23 @@ decide-is-negative-is-nonnegative-ℤ (inl x) = inl star
 decide-is-negative-is-nonnegative-ℤ (inr x) = inr star
 ```
 
-Legacy (Used in Bezout's lemma)
+#### An integer or its negative is nonnegative
 
 ```agda
-decide-is-nonnegative-ℤ :
+decide-is-nonnegative-is-nonnegative-neg-ℤ :
   {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x))
-decide-is-nonnegative-ℤ {inl x} = inr star
-decide-is-nonnegative-ℤ {inr x} = inl star
+decide-is-nonnegative-is-nonnegative-neg-ℤ {inl x} = inr star
+decide-is-nonnegative-is-nonnegative-neg-ℤ {inr x} = inl star
+```
 
-is-zero-is-nonnegative-neg-is-nonnegative-ℤ :
-  (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x
-is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos =
-  refl
+#### An integer or its negative is nonpositive
+
+```agda
+decide-is-nonpositive-is-nonpositive-neg-ℤ :
+  {x : ℤ} → (is-nonpositive-ℤ x) + (is-nonpositive-ℤ (neg-ℤ x))
+decide-is-nonpositive-is-nonpositive-neg-ℤ {inl x} = inl star
+decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inl x)} = inl star
+decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inr x)} = inr star
 ```
 
 ### Inclusion properties