diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr index 6ff12e4cbd..4db366940e 100644 --- a/libs/prelude/Prelude/Types.idr +++ b/libs/prelude/Prelude/Types.idr @@ -39,7 +39,7 @@ nonNegativeIntegerToNat : nonNegativeIntegerToNat 0 = Z nonNegativeIntegerToNat x = let -- x >= 0 and x != 0 - -- so x >= 0 so x - 1 >= 0 + -- so x > 0 so x - 1 >= 0 prf = believe_me Refl in S $ nonNegativeIntegerToNat {prf} $ assert_smaller x $ x - 1