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