A function returning a value in a dependent type

Define a function with a dependent type that returns true for natural numbers of the form 4n+1, false for numbers of the form 4n+3 and n for numbers of the form 2n.

Solution

This file