feat: have Ord imply LT/LE

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))