rw [← Nat.log_mul hb hn]
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ ?a.b✝

case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b (b * n + c)

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n) ≤ log b (b * n + c)