exact absurd ‹step n₁ ≃ 0› step_neqv_zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ + m ≃ y + m
n₂ : ℕ
x✝ : step n₁ ≃ 0
⊢ step n₁ + m ≃ 0 + m
no goals