exact absurd ‹step (n + d) ≃ 0› step_neqv_zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n < 0
this✝ : step n ≤ 0
d : ℕ
h✝ : step n + d ≃ 0
this : step (n + d) ≃ 0
⊢ False
no goals