fibIterative : Nat -> Nat
fibIterative n = fibIterative' n Z (S Z)
  where fibIterative' : Nat -> Nat -> Nat -> Nat
        fibIterative' Z a _ = a
        fibIterative' (S n) a b = fibIterative' n b (a + b)