# Defining a discrete log function by iteration

Define the `log2` function by iteration
and prove that it satisfies the following property:

forall n:nat, n > 0 -> two_power (log2 n) <= n < 2 * two_power (log2 n)

## Solution

Follow this link

Going home

Yves Bertot
Last modified: Sun Feb 29 13:06:34 MET 2004