Logarithm and power
Define a function
power:Z ->nat ->Z
to compute the power of an integer and a function
discrete_log:positive->nat
that maps any number
p
to its discrete logarithm (with base 2).
Solution
Look at
this file