norm_cast
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ ↑b
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
hlogb_nonneg : 0 ≤ (↑b).logb ↑n
⊢ 1 ≤ b