intro p hbp _ hp
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
hbp : a < p
a✝ : p ≤ b
hp : Nat.Prime p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p