diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
index 029176b1d5..0a1461245f 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
@@ -840,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