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

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