linarith [Nat.floor_le hlogb_nonneg]
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
hlogb_nonneg : 0 ≤ Real.logb 2 ↑N
⊢ ↑⌊Real.logb 2 ↑N⌋₊ + 1 ≤ 1 + Real.logb 2 ↑N
no goals