Division by 4

Define a function of type positive->Z that maps every number p to the integer part of p/4

Solution

Look at this file