On the list 1::2:: ... n::nil

Build a function computing the list 1::2:: ... n::nil for every n of type nat.

Solution

Look at this file

Note

This solution uses an anonymous recursive function (with fix). If you want to prove some properties of the main function, it could be useful to give a name to this auxiliary function (i.e to define it with Fixpoint).