p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1
p n k : ℕ
p_large : n < p ^ 2
⊢ ↑(factorization (choose n k)) p ≤ 1
apply factorization_choose_le_log.trans
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1
p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1
rcases eq_or_ne n 0 with (rfl | hn0)
no goals
case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1
exact lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)
no goals
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1
simp