b x : ℕ
hb : 1 < b
z : ℕ
⊢ b ^ x ≤ b ^ z ↔ x ≤ z
b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z
rw [← le_pow_iff_clog_le hb]
no goals
b x : ℕ
hb : 1 < b
z : ℕ
⊢ b ^ x ≤ b ^ z ↔ x ≤ z
exact (pow_right_strictMono hb).le_iff_le