apply Real.rpow_lt_rpow _ _ (by norm_num)
n : ℝ
hn : 32 ≤ n
⊢ ((2 * n) ^ 6⁻¹) ^ 6 < (↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1