intro p _
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ∈ Finset.Ioc a b
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≠ 1 → Nat.Prime p