case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0

case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ ↑(factorization (choose n k)) p = 0
p n k : ℕ
h : n < p
⊢ ↑(factorization (choose n k)) p = 0
by_cases hnk : n < k
no goals
case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ ↑(factorization (choose n k)) p = 0
rw [choose_eq_factorial_div_factorial (le_of_not_lt hnk),
  factorization_div (factorial_mul_factorial_dvd_factorial (le_of_not_lt hnk)), Finsupp.coe_tsub,
  Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]
no goals
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
simp [choose_eq_zero_of_lt hnk]