diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
index 029176b1d5..ec29631deb 100644
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@@ -72,12 +72,13 @@ mult (S left) right = plus right $ mult left right
 
 ||| Convert an Integer to a Nat, mapping negative numbers to 0
 fromIntegerNat : Integer -> Nat
-fromIntegerNat 0 = Z
-fromIntegerNat n =
-  if (n > 0) then
-    S (fromIntegerNat (assert_smaller n (n - 1)))
-  else
-    Z
+fromIntegerNat i = 
+  case (i > 0) of 
+    True  => S (fromIntegerNat (assert_smaller i (i - 1)))
+    False => Z
+-- Using if here would cause infinite looping in some cases.
+-- This could be fixed by redundantly matching on 0 explicitly, but that would stop
+--   fromIntegerNat from reducing in proofs.
 
 ||| Convert a Nat to an Integer
 toIntegerNat : Nat -> Integer