import Nat

fun log(n) {
  find_log(n, ℕ0, ℕ0)
}

less_equal_pow_log: (all n:Nat. n ≤ pow2(log(n)))