gcongr
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ (2 * ↑n).sqrt * 4 ^ (2 * ↑n / 3)
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n

case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ (2 * ↑n).sqrt

case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4

case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3