From 5e30f210d4d510649ca87a02b7e9a409ee74d13a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 20 Feb 2024 21:23:29 -0600
Subject: Prove merge lemmas

---
 FinMerge.agda | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

(limited to 'FinMerge.agda')

diff --git a/FinMerge.agda b/FinMerge.agda
index b483fc8..f237a53 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -12,16 +12,8 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-R
 open import Function using (id ; _∘_ ; _$_)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 
+open import Util using (_<_<_; _<_≤_; toℕ<)
 
-_<_≤_ : ℕ → ℕ → ℕ → Set
-_<_≤_ i j k = (i < j) × (j ≤ k)
-
-_<_<_ : ℕ → ℕ → ℕ → Set
-_<_<_ i j k = (i < j) × (j < k)
-
-toℕ< : {n : ℕ} → (i : Fin n) → toℕ i < n
-toℕ< Fin.zero = z<s
-toℕ< (Fin.suc i) = _≤_.s≤s (toℕ< i)
 
 data Ordering {n : ℕ} : Fin n → Fin n → Set where
   less : ∀ {i j} → toℕ i < toℕ j < n → Ordering i j
-- 
cgit v1.2.3