case zero
p n k : ℕ
h✝ : n < p
h : zero < p
⊢ ↑(factorization zero !) p = 0

case succ
p n✝ k : ℕ
h✝ : n✝ < p
n : ℕ
hn : n < p → ↑(factorization n !) p = 0
h : succ n < p
⊢ ↑(factorization (succ n)!) p = 0
p n k : ℕ
h : n < p
⊢ ↑(factorization n !) p = 0
induction' n with n hn
no goals
case succ
p n✝ k : ℕ
h✝ : n✝ < p
n : ℕ
hn : n < p → ↑(factorization n !) p = 0
h : succ n < p
⊢ ↑(factorization (succ n)!) p = 0
rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add,
  Pi.add_apply, hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
no goals
case zero
p n k : ℕ
h✝ : n < p
h : zero < p
⊢ ↑(factorization zero !) p = 0
simp