From edefbbd6cc457a6b06f9d5e91867ef101776503b Mon Sep 17 00:00:00 2001
From: Leif Warner <abimelech@gmail.com>
Date: Wed, 25 Apr 2018 08:15:47 -0700
Subject: [PATCH 1/2] =?UTF-8?q?Added=20Not=20(i=20=E2=89=A4=20j)=20->=20i?=
 =?UTF-8?q?=20>=20j?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 libs/prelude/Prelude/Nat.idr | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
index 029176b1d5..99e1971f47 100644
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@@ -149,9 +149,9 @@ fromLteSucc (LTESucc x) = x
 isLTE : (m, n : Nat) -> Dec (m `LTE` n)
 isLTE Z n = Yes LTEZero
 isLTE (S k) Z = No succNotLTEzero
-isLTE (S k) (S j) with (isLTE k j)
-  isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)
-  isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)
+isLTE (S k) (S j) = case isLTE k j of
+  Yes prf => Yes (LTESucc prf)
+  No contra => No (contra . fromLteSucc)
 
 ||| `LTE` is reflexive.
 lteRefl : LTE n n
@@ -182,6 +182,12 @@ notLTImpliesGTE {b = Z} _ = LTEZero
 notLTImpliesGTE {a = Z} {b = S k} notLt = absurd (notLt (LTESucc LTEZero))
 notLTImpliesGTE {a = S k} {b = S j} notLt = LTESucc (notLTImpliesGTE (notLt . LTESucc))
 
+||| If a number is not less than or equal to another, it is greater than it
+notLTEImpliesGT : Not (i `LTE` j) -> i `GT` j
+notLTEImpliesGT {i = Z}             notLt = absurd $ notLt LTEZero
+notLTEImpliesGT {i = S k} {j = Z}   _     = LTESucc LTEZero
+notLTEImpliesGT {i = S j} {j = S k} notLt = LTESucc (notLTEImpliesGT (notLt . LTESucc))
+
 ||| Boolean test than one Nat is less than or equal to another
 total lte : Nat -> Nat -> Bool
 lte Z        right     = True

From d406219e0d0608df3664bd13ab00d4523d747a32 Mon Sep 17 00:00:00 2001
From: Leif Warner <abimelech@gmail.com>
Date: Wed, 25 Apr 2018 08:21:32 -0700
Subject: [PATCH 2/2] Added an implication from GTE to maximum.

---
 libs/prelude/Prelude/Nat.idr | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
index 99e1971f47..0a1461245f 100644
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@@ -846,3 +846,9 @@ sucMinL (S l) = cong (sucMinL l)
 total sucMinR : (l : Nat) -> minimum l (S l) = l
 sucMinR Z = Refl
 sucMinR (S l) = cong (sucMinR l)
+
+||| If one number is biggre than another, you know what the maximum is.
+total lteImpliesMax : i `LTE` j -> maximum i j = j
+lteImpliesMax {i = Z}             _           = Refl
+lteImpliesMax {i = S k} {j = Z}   _           impossible
+lteImpliesMax {i = S k} {j = S j} (LTESucc x) = cong {f = S} $ lteImpliesMax x