Rename < and <' proofs in Data.Integer.Properties (#1112)

Author: MatthewDaggitt

CHANGELOG.md

@@ -266,11 +266,6 @@ attached to all deprecated names to discourage their use.
   decSetoid        ↦ ≡-decSetoid
   ```
 
-* In `Data.Integer.Properties`:
-  ```agda
-  [1+m]*n≡n+m*n ↦ suc-*
-  ```
-
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   Any¬→¬All  ↦  Any¬⇒¬All
@@ -605,6 +600,12 @@ Other minor additions
   ∣p∣⊔∣q∣≤∣p∪q∣ : ∣ p ∣ ⊔ ∣ q ∣ ≤ ∣ p ∪ q ∣
   ```
 
+* Added new proofs to `Data.Integer.Properties`:
+  ```agda
+  suc[i]≤j⇒i<j : sucℤ i ≤ j → i < j
+  i<j⇒suc[i]≤j : i < j → sucℤ i ≤ j
+  ```
+
 * Added new proofs to `Data.Maybe.Properties`:
   ```agda
   map-nothing : ma ≡ nothing → map f ma ≡ nothing

src/Data/Integer/Properties.agda

@@ -945,17 +945,17 @@ suc-mono (-≤+ {m}) = 0⊖m≤+ m
 suc-mono (-≤- n≤m) = ⊖-monoʳ-≥-≤ zero n≤m
 suc-mono (+≤+ m≤n) = +≤+ (s≤s m≤n)
 
-m+1≤n⇒m<n : ∀ {m n} → sucℤ m ≤ n → m < n
-m+1≤n⇒m<n {+ m}           {+ _}       (+≤+ m≤n) = +<+ m≤n
-m+1≤n⇒m<n { -[1+ 0 ]}     {+ n}       p         = -<+
-m+1≤n⇒m<n { -[1+ suc m ]} {+ n}       -≤+       = -<+
-m+1≤n⇒m<n { -[1+ suc m ]} { -[1+ n ]} (-≤- n≤m) = -<- (ℕ.s≤s n≤m)
-
-m<n⇒m+1≤n : ∀ {m n} → m < n → sucℤ m ≤ n
-m<n⇒m+1≤n {+ _}           {+ _}       (+<+ m<n) = +≤+ m<n
-m<n⇒m+1≤n { -[1+ 0 ]}     {+ _}       -<+       = +≤+ z≤n
-m<n⇒m+1≤n { -[1+ suc m ]} { -[1+ _ ]} (-<- n<m) = -≤- (ℕ.≤-pred n<m)
-m<n⇒m+1≤n { -[1+ suc m ]} {+ _}       -<+       = -≤+
+suc[i]≤j⇒i<j : ∀ {i j} → sucℤ i ≤ j → i < j
+suc[i]≤j⇒i<j {+ i}           {+ _}       (+≤+ i≤j) = +<+ i≤j
+suc[i]≤j⇒i<j { -[1+ 0 ]}     {+ j}       p         = -<+
+suc[i]≤j⇒i<j { -[1+ suc i ]} {+ j}       -≤+       = -<+
+suc[i]≤j⇒i<j { -[1+ suc i ]} { -[1+ j ]} (-≤- j≤i) = -<- (ℕ.s≤s j≤i)
+
+i<j⇒suc[i]≤j : ∀ {i j} → i < j → sucℤ i ≤ j
+i<j⇒suc[i]≤j {+ _}           {+ _}       (+<+ i<j) = +≤+ i<j
+i<j⇒suc[i]≤j { -[1+ 0 ]}     {+ _}       -<+       = +≤+ z≤n
+i<j⇒suc[i]≤j { -[1+ suc i ]} { -[1+ _ ]} (-<- j<i) = -≤- (ℕ.≤-pred j<i)
+i<j⇒suc[i]≤j { -[1+ suc i ]} {+ _}       -<+       = -≤+
 
 ------------------------------------------------------------------------
 -- Properties of pred
@@ -1901,6 +1901,6 @@ Please use _<_ instead."
 
 [1+m]*n≡n+m*n = suc-*
 {-# WARNING_ON_USAGE [1+m]*n≡n+m*n
-"Warning: [1+m]*n≡n+m*n was deprecated in v1.1.
+"Warning: [1+m]*n≡n+m*n was deprecated in v1.2.
 Please use suc-* instead."
 #-}