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)}