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