rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : ¬(x.Prime ∧ n < x ∧ x ≤ 2 * n)
⊢ x ^ n.centralBinom.factorization x = 1
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬x.Prime ∨ x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1