@@ -160,6 +160,11 @@ lteAddRight : (n : Nat) -> LTE n (plus n m)
160160lteAddRight Z = LTEZero
161161lteAddRight (S k) = LTESucc (lteAddRight k)
162162
163+||| If a number is not less than another, it is greater than or equal to it
164+notLTImpliesGTE : Not (LT a b) -> GTE a b
165+notLTImpliesGTE {b = Z} _ = LTEZero
166+notLTImpliesGTE {a = Z} {b = S k} notLt = absurd (notLt (LTESucc LTEZero))
167+notLTImpliesGTE {a = S k} {b = S j} notLt = LTESucc (notLTImpliesGTE (notLt . LTESucc))
163168
164169||| Boolean test than one Nat is less than or equal to another
165170total lte : Nat -> Nat -> Bool