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

---
 Util.agda | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 Util.agda

(limited to 'Util.agda')

diff --git a/Util.agda b/Util.agda
new file mode 100644
index 0000000..23da7cc
--- /dev/null
+++ b/Util.agda
@@ -0,0 +1,16 @@
+module Util where
+
+open import Data.Fin using (Fin; toℕ)
+open import Data.Nat using (ℕ; _≤_; _<_ ; z<s; s≤s)
+open import Data.Product using (_×_)
+
+
+_<_≤_ : ℕ → ℕ → ℕ → 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)
-- 
cgit v1.2.3