apply cases_on (motive := λ n => n + m ≃ 0 → n ≃ 0 ∧ m ≃ 0) n
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + m ≃ 0 → n ≃ 0 ∧ m ≃ 0
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + m ≃ 0 → 0 ≃ 0 ∧ m ≃ 0

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0