From bef7264302bff7d65d8732dd458d198be865812a Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 12 Mar 2025 12:52:08 -0400
Subject: [PATCH 1/2] =?UTF-8?q?[Refractor]=20=E2=8A=A5-elim=20to=20contrad?=
 =?UTF-8?q?iction1=20in=20asym=E2=87=92antisym=20def?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Binary/Consequences.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 3cdb4db356..812f808fbd 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -15,7 +15,7 @@ open import Function.Base using (_∘_; _∘₂_; _$_; flip)
 open import Level using (Level)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable.Core
   using (yes; no; recompute; map′; dec⇒maybe)
 open import Relation.Unary using (∁; Pred)
@@ -121,8 +121,8 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
     irrefl (antisym x<y y<x) x<y
 
   asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
-  asym⇒antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
-
+  asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y) 
+ 
   asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
              Asymmetric _<_ → Irreflexive _≈_ _<_
   asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =

From 62a09e8f8146bf9aa4686d02b31178d97a5a2d2b Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 12 Mar 2025 14:31:52 -0400
Subject: [PATCH 2/2] fix-whitespace

---
 src/Relation/Binary/Consequences.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 812f808fbd..f82d30f1aa 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -121,8 +121,8 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
     irrefl (antisym x<y y<x) x<y
 
   asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
-  asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y) 
- 
+  asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y)
+
   asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
              Asymmetric _<_ → Irreflexive _≈_ _<_
   asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =