rw [factorization_eq_zero_of_non_prime n.centralBinom h, Nat.pow_zero]
case hf.inl
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬x.Prime ∨ x ≤ n
h : ¬x.Prime
⊢ x ^ n.centralBinom.factorization x = 1
no goals