@@ -136,9 +136,9 @@ lteRefl {n = Z} = LTEZero
136lteRefl {n = S k} = LTESucc lteRefl
136lteRefl {n = S k} = LTESucc lteRefl
138||| n < m implies n < m + 1
138||| n < m implies n < m + 1
139−lteSucc : LTE n m -> LTE n (S m)
139+lteSuccRight : LTE n m -> LTE n (S m)
140−lteSucc LTEZero = LTEZero
140+lteSuccRight LTEZero = LTEZero
141−lteSucc (LTESucc x) = LTESucc (lteSucc x)
141+lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
144||| Boolean test than one Nat is less than or equal to another
144||| Boolean test than one Nat is less than or equal to another