case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n
rcases eq_or_ne n 0 with (rfl | hn)
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n
apply le_log_of_pow_le hc
no goals
case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ c ^ log b n ≤ n
calc
  c ^ log b n ≤ b ^ log b n := pow_le_pow_of_le_left' hb _
  _ ≤ n := pow_log_le_self _ hn
no goals
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0
rw [log_zero_right, log_zero_right]