From a30b226b20ade43e23c4fcd27b0247afe48d56cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Fri, 13 Sep 2024 09:29:09 -0300
Subject: [PATCH] =?UTF-8?q?fixup=20neg=E2=84=A4-<=20name?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Int/Order.lagda.md           | 19 ++++++++++---------
 src/Data/Rational/Properties.lagda.md | 10 +++++-----
 2 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/Data/Int/Order.lagda.md b/src/Data/Int/Order.lagda.md
index ae9f2de0a..97fa46bf0 100644
--- a/src/Data/Int/Order.lagda.md
+++ b/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)
+```
diff --git a/src/Data/Rational/Properties.lagda.md b/src/Data/Rational/Properties.lagda.md
index 4c09868bf..3e9c692d1 100644
--- a/src/Data/Rational/Properties.lagda.md
+++ b/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 α))
 ```