Define the functional which maps a function f from
nat to Z to the sum
Look at this file
The solution comes with a little example, which uses some tactics
to control the relationship between nat and Z.