b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b n
rw [clog_of_two_le hb hn]
no goals
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1
exact zero_lt_succ _