have H3 : n.centralBinom ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) :=
  centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_big) no_prime
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False