have h0 : 0 ≤ (2 * n) ^ 6⁻¹
n : ℝ
hn : 32 ≤ n
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹