Idris: totality check fails when trying to re-implement fromInteger for Nat

I have the following code:

module Test
  data Nat' = S' Nat' | Z'
  Num Nat' where
    x * y = ?hole
    x + y = ?hole
    fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1))

I get an error message about the last line:

Test.idr:6:5:
Prelude.Interfaces.Test.Nat' implementation of Prelude.Interfaces.Num, method fromInteger is
possibly not total due to recursive path Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger --> Prelude.Interfaces.Test.Nat' implementation of
Prelude.Interfaces.Num, method fromInteger

The function should always give a result, because eventually the argument of fromInteger will become small enough to pick the first case. But Idris does not seem to understand this. What is wrong with this function, and how can I fix this error?

n - 1 is not structurally smaller than n, to see this just observe that Integer is not an inductive type. Thus, you need to convince the totality checker your function is actually total using a trick like assert_smaller (see the Idris tutorial):

Here is its current definition:

 assert_smaller : (x : a) -> (y : b) -> b
 assert_smaller x y = y

It simply evaluates to its second argument, but also asserts to the totality checker that y is structurally smaller than x.

This is what Idris uses in its standard library (see here) for your problem:

fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z