Computing f(0)+f(1)+...f(n)

Define the functional which maps a function f from nat to Z to the sum f(0)+f(1)+...f(n)

Solution

The solution comes with a little example, which uses some tactics to control the relationship between nat and Z.