rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]
case hf.inr
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 ≤ n
⊢ x ^ n.centralBinom.factorization x = 1
no goals