rw [mul_lt_mul_right (by apply sq_pos_of_pos; linarith)]
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n * (2 * n) ^ 2 < 8000 * (2 * n) ^ 2 ↔ n < 4000
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 8000 ↔ n < 4000