b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ pred (clog b x) < clog b x
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ pred (clog b x) < x
rw [← not_le, le_pow_iff_clog_le hb, not_le]
no goals
b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ pred (clog b x) < clog b x
exact pred_lt (clog_pos hb hx).ne'