fixup negℤ-< name

src/Data/Int/Order.lagda.md

@@ -439,12 +439,13 @@ abstract
     (*ℤ-preserves-≤r {x} {y} z (<-weaken x<y))
     λ xz=yz → <-irrefl (*ℤ-injectiver z x y (positive→nonzero auto) xz=yz) x<y
 
-  negℤ-< : ∀ {x y} → x < y → negℤ y < negℤ x
-  negℤ-< {posz} {pos y} (pos<pos (Nat.s≤s p)) = neg<pos
-  negℤ-< {possuc x} {pos y} (pos<pos (Nat.s≤s p)) = neg<neg p
-  negℤ-< {negsuc x} {posz} neg<pos = pos<pos (Nat.s≤s Nat.0≤x)
-  negℤ-< {negsuc x} {possuc y} neg<pos = neg<pos
-  negℤ-< {negsuc x} {negsuc y} (neg<neg p) = pos<pos (Nat.s≤s p)
-
-  <-negℤ : ∀ {x y} → negℤ x < negℤ y → y < x
-  <-negℤ {x} {y} p = subst₂ _<_ (negℤ-negℤ y) (negℤ-negℤ x) (negℤ-< p)
+  negℤ-anti-< : ∀ {x y} → x < y → negℤ y < negℤ x
+  negℤ-anti-< {posz} {pos y} (pos<pos (Nat.s≤s p)) = neg<pos
+  negℤ-anti-< {possuc x} {pos y} (pos<pos (Nat.s≤s p)) = neg<neg p
+  negℤ-anti-< {negsuc x} {posz} neg<pos = pos<pos (Nat.s≤s Nat.0≤x)
+  negℤ-anti-< {negsuc x} {possuc y} neg<pos = neg<pos
+  negℤ-anti-< {negsuc x} {negsuc y} (neg<neg p) = pos<pos (Nat.s≤s p)
+
+  negℤ-anti-full-< : ∀ {x y} → negℤ x < negℤ y → y < x
+  negℤ-anti-full-< {x} {y} p = subst₂ _<_ (negℤ-negℤ y) (negℤ-negℤ x) (negℤ-anti-< p)
+```

src/Data/Rational/Properties.lagda.md

@@ -215,10 +215,10 @@ abstract
 
 ```agda
 abstract
-  negℚ-< : ∀ {x y} → x < y → -ℚ y < -ℚ x
-  <-negℚ : ∀ {x y} → -ℚ x < -ℚ y → y < x
+  negℚ-anti-< : ∀ {x y} → x < y → -ℚ y < -ℚ x
+  negℚ-anti-full-< : ∀ {x y} → -ℚ x < -ℚ y → y < x
 
-  unquoteDef negℚ-< <-negℚ = do
-    by-elim-ℚ negℚ-< λ d x y α → common-denom-< (ℤ.negℤ-< (<-common-denom α))
-    by-elim-ℚ <-negℚ λ d x y α → common-denom-< (ℤ.<-negℤ (<-common-denom α))
+  unquoteDef negℚ-anti-< negℚ-anti-full-< = do
+    by-elim-ℚ negℚ-anti-< λ d x y α → common-denom-< (ℤ.negℤ-anti-< (<-common-denom α))
+    by-elim-ℚ negℚ-anti-full-< λ d x y α → common-denom-< (ℤ.negℤ-anti-full-< (<-common-denom α))
 ```