@@ -161,10 +161,10 @@ lteAddRight Z = LTEZero
161161lteAddRight (S k) = LTESucc (lteAddRight k)
162162
163163||| If a number is not less than another, it is greater than or equal to it
164−ifNotLtThenGte : Not (LT a b) -> GTE a b
165−ifNotLtThenGte {b = Z} _ = LTEZero
166−ifNotLtThenGte {a = Z} {b = S k} notLt = absurd (notLt (LTESucc LTEZero))
167−ifNotLtThenGte {a = S k} {b = S j} notLt = LTESucc (ifNotLtThenGte (notLt . LTESucc))
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))
168168
169169||| Boolean test than one Nat is less than or equal to another
170170total lte : Nat -> Nat -> Bool