# Discrete logarithm

Using the function `two_power` defined for the exercise
about computing the power of 2.
and well-founded recursion, define a function that satisfies the following
specification:

forall n:nat, n <> 0 ->
{p : nat | two_power p <= n /\ n < two_power (p + 1)}

## Solution

Follow this link

Going home

Pierre Castéran