apply le_antisymm
case neg
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
⊢ b.log n = ⌊(↑b).logb ↑n⌋₊
case neg.a
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
⊢ b.log n ≤ ⌊(↑b).logb ↑n⌋₊

case neg.a
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
⊢ ⌊(↑b).logb ↑n⌋₊ ≤ b.log n