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

Going home

Pierre Castéran