case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1

case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1
b n : ℕ
⊢ log b (n / b) = log b n - 1
cases' le_or_lt b 1 with hb hb
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1

case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b) = log b n - 1
cases' lt_or_le n b with h h
no goals
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b) = log b n - 1
rw [log_of_one_lt_of_le hb h, add_tsub_cancel_right]
no goals
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b) = log b n - 1
rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
no goals
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b) = log b n - 1
rw [div_eq_of_lt h, log_of_lt h, log_zero_right]