Added extra ordering relations to Data.Integer and improved compatability of Data.Integer.Properties with planned changes to Data.Integer

Author: Matthew Daggitt

CHANGELOG.md

@@ -235,6 +235,17 @@ Backwards compatible changes
   ∩⇔×       : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
   ```
 
+* Added relations to `Data.Integer`
+  ```agda
+  _≥_ : Rel ℤ _
+  _<_ : Rel ℤ _
+  _>_ : Rel ℤ _
+  _≰_ : Rel ℤ _
+  _≱_ : Rel ℤ _
+  _≮_ : Rel ℤ _
+  _≯_ : Rel ℤ _
+  ```
+
 * Added proofs to `Data.Integer.Properties`
   ```agda
   +-injective           : + m ≡ + n → m ≡ n
@@ -260,6 +271,7 @@ Backwards compatible changes
   +-inverse             : Inverse (+ 0) -_ _+_
   +-0-isMonoid          : IsMonoid _≡_ _+_ (+ 0)
   +-0-isGroup           : IsGroup _≡_ _+_ (+ 0) (-_)
+  +-0-abelianGroup      : AbelianGroup _ _
   neg-distrib-+         : - (m + n) ≡ (- m) + (- n)
   ◃-distrib-+           : s ◃ (m + n) ≡ (s ◃ m) + (s ◃ n)
 

src/Data/Integer/Base.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.Core using (_≡_; refl)
 infix  8 -_
 infixl 7 _*_ _⊓_
 infixl 6 _+_ _-_ _⊖_ _⊔_
-infix  4 _≤_
+infix  4 _≤_ _≥_ _<_ _>_ _≰_ _≱_ _≮_ _≯_
 
 ------------------------------------------------------------------------
 -- The types
@@ -149,6 +149,27 @@ data _≤_ : ℤ → ℤ → Set where
   -≤- : ∀ {m n} → (n≤m : n ℕ.≤ m) → -[1+ m ] ≤ -[1+ n ]
   +≤+ : ∀ {m n} → (m≤n : m ℕ.≤ n) → + m ≤ + n
 
+_≥_ : Rel ℤ _
+x ≥ y = y ≤ x
+
+_<_ : Rel ℤ _
+x < y = suc x ≤ y
+
+_>_ : Rel ℤ _
+x > y = y < x
+
+_≰_ : Rel ℤ _
+x ≰ y = ¬ (x ≤ y)
+
+_≱_ : Rel ℤ _
+x ≱ y = ¬ (x ≥ y)
+
+_≮_ : Rel ℤ _
+x ≮ y = ¬ (x < y)
+
+_≯_ : Rel ℤ _
+x ≯ y = ¬ (x > y)
+
 drop‿+≤+ : ∀ {m n} → + m ≤ + n → ℕ._≤_ m n
 drop‿+≤+ (+≤+ m≤n) = m≤n