case step =>
  intro n (_ : step n + m ≃ 0)
  show step n ≃ 0 ∧ m ≃ 0
  apply False.elim
  show False
  have : step (n + m) ≃ step n + m := Rel.symm Addition.step_add
  have : step (n + m) ≃ 0 :=
    Rel.trans ‹step (n + m) ≃ step n + m› ‹step n + m ≃ 0›
  exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0
no goals