apply ltTwoMulSqrtTwoMul
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 < 2 * Real.sqrt (2 * n)
case h
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 81 / 2 < n