Using the function exp2 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 | exp2 p <= n /\ n < exp2 (p + 1)}