rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
⊢ x ^ n.centralBinom.factorization x = 1
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ x ^ n.centralBinom.factorization x = 1