rw [@Real.rpow_add (2*n) (by linarith)]
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ (1 + 2) < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000