rw [Nat.sqrt_lt'] at hbp
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1