From 37dcbf34210d164b2bba657f18c7dd9762717e86 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 28 May 2021 14:08:50 +0200
Subject: [PATCH] feat: have `Ord` imply `LT/LE`

---
 src/Init/Data/Ord.lean | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index dfd33b34c7..e6a836aaf1 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Dany Fabian
+Authors: Dany Fabian, Sebastian Ullrich
 -/
 
 prelude
@@ -58,3 +58,21 @@ instance : Ord USize where
 
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
+
+
+instance [Ord α] : LT α where
+  lt a b := compare a b == Ordering.lt
+
+instance [Ord α] : DecidableRel (@LT.lt α _) :=
+  inferInstanceAs (DecidableRel (fun a b => compare a b == Ordering.lt))
+
+def Ordering.isLE : Ordering → Bool
+  | Ordering.lt => true
+  | Ordering.eq => true
+  | Ordering.gt => false
+
+instance [Ord α] : LE α where
+  le a b := (compare a b).isLE
+
+instance [Ord α] : DecidableRel (@LE.le α _) :=
+  inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))