case zero
n : ℕ
h : n ∈ divisors zero
⊢ n ∣ zero

case succ
n n✝ : ℕ
h : n ∈ divisors (succ n✝)
⊢ n ∣ succ n✝
n m : ℕ
h : n ∈ divisors m
⊢ n ∣ m
cases m
no goals
case zero
n : ℕ
h : n ∈ divisors zero
⊢ n ∣ zero
apply dvd_zero
no goals
case succ
n n✝ : ℕ
h : n ∈ divisors (succ n✝)
⊢ n ∣ succ n✝
simp [mem_divisors.1 h]