case inl
p : ℕ
h : p ∈ factors 0
⊢ p ∣ 0

case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ∣ n
n p : ℕ
h : p ∈ factors n
⊢ p ∣ n
rcases n.eq_zero_or_pos with (rfl | hn)
no goals
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ∣ 0
exact dvd_zero p
no goals
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ∣ n
rwa [← mem_factors_iff_dvd hn.ne' (prime_of_mem_factors h)]