case zero
n : ℕ
h : zero ∈ divisors n
⊢ 0 < zero

case succ
n n✝ : ℕ
h : succ n✝ ∈ divisors n
⊢ 0 < succ n✝
n m : ℕ
h : m ∈ divisors n
⊢ 0 < m
cases m
no goals
case succ
n n✝ : ℕ
h : succ n✝ ∈ divisors n
⊢ 0 < succ n✝
apply Nat.succ_pos
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < zero
case zero
n : ℕ
h : zero ∈ divisors n
⊢ 0 < zero
rw [mem_divisors, zero_eq, zero_dvd_iff (a := n)] at h
no goals
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < zero
cases h.2 h.1