case zero
n : ℕ
⊢ n ∈ divisors zero → n ≤ zero

case succ
n m : ℕ
⊢ n ∈ divisors (succ m) → n ≤ succ m
n m : ℕ
⊢ n ∈ divisors m → n ≤ m
cases' m with m
no goals
case zero
n : ℕ
⊢ n ∈ divisors zero → n ≤ zero
simp
case succ
n m : ℕ
⊢ n ∣ succ m → n ≤ succ m
case succ
n m : ℕ
⊢ n ∈ divisors (succ m) → n ≤ succ m
simp only [mem_divisors, Nat.succ_ne_zero m, and_true_iff, Ne.def, not_false_iff]
no goals
case succ
n m : ℕ
⊢ n ∣ succ m → n ≤ succ m
exact Nat.le_of_dvd (Nat.succ_pos m)