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)
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
case inl
p : ℕ
h : p ∈ factors 0
⊢ p ≤ 0
rw [factors_zero] at h
no goals
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
cases h
no goals
case inr
n p : ℕ
h : p ∈ factors n
hn : n > 0
⊢ p ≤ n
exact le_of_dvd hn (dvd_of_mem_factors h)