b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n
rw [← le_pow_iff_clog_le (lt_of_lt_of_le hc hb)]
no goals
b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ n ≤ b ^ clog c n
calc
  n ≤ c ^ clog c n := le_pow_clog hc _
  _ ≤ b ^ clog c n := pow_le_pow_of_le_left hb _