apply (mul_one _).symm
case h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b = ?b

case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?b ≤ b * n

case b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

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

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

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

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