apply le_trans (Nat.factorization_choose_le_log)
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ Nat.log p (2 * n) ≤ 1