[Refractor] contradiction over ⊥-elim in ×-antisymmetric def

Author: jmougeot

src/Data/Product/Relation/Binary/Lex/NonStrict.agda

@@ -12,6 +12,9 @@
 module Data.Product.Relation.Binary.Lex.NonStrict where
 
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
+  using (Pointwise)
+import Data.Product.Relation.Binary.Lex.Strict as Strict
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _⇒_)
@@ -24,9 +27,7 @@ open import Relation.Binary.Definitions
         ; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences
 import Relation.Binary.Construct.NonStrictToStrict as Conv
-open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
-import Data.Product.Relation.Binary.Lex.Strict as Strict
+
 
 private
   variable

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -15,11 +15,9 @@ open import Data.Product.Base
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
   using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
-open import Data.Empty using (⊥-elim)
 open import Function.Base using (flip; _on_; _$_; _∘_)
 open import Induction.WellFounded using (Acc; acc; WfRec; WellFounded; Acc-resp-flip-≈)
 open import Level using (Level)
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Preorder; StrictPartialOrder; StrictTotalOrder)
@@ -31,6 +29,8 @@ open import Relation.Binary.Definitions
         ; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Negation using (contradiction)
 
 private
   variable
@@ -134,11 +134,11 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
     where
     antisym : Antisymmetric _≋_ _<ₗₑₓ_
     antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
-      ⊥-elim $ asym₁ x₁<y₁ y₁<x₁
+      contradiction y₁<x₁ (asym₁ x₁<y₁)
     antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
-      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ y≈≤x) x₁<y₁
+      contradiction x₁<y₁ (irrefl₁ (sym₁ $ proj₁ y≈≤x))
     antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) =
-      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ x≈≤y) y₁<x₁
+      contradiction y₁<x₁ (irrefl₁ (sym₁ $ proj₁ x≈≤y))
     antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
       proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)