have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_big
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)