@@ -110,6 +110,22 @@ LT left right = LTE (S left) right
110110total GT : Nat -> Nat -> Type
111111GT left right = LT right left
112112
113+||| A successor is never less than or equal zero
114+succNotLTEzero : Not (S m `LTE` Z)
115+succNotLTEzero lteZero impossible
116+
117+||| If two numbers are ordered, their predecessors are too
118+fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)
119+fromLteSucc (lteSucc x) = x
120+
121+||| A decision procedure for `LTE`
122+isLTE : (m, n : Nat) -> Dec (m `LTE` n)
123+isLTE Z n = Yes lteZero
124+isLTE (S k) Z = No succNotLTEzero
125+isLTE (S k) (S j) with (isLTE k j)
126+ isLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)
127+ isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)
128+
113129||| Boolean test than one Nat is less than or equal to another
114130total lte : Nat -> Nat -> Bool
115131lte Z right = True