have : step (n + d) ≃ 0 := calc
  step (n + d) ≃ _ := Rel.symm step_add
  step n + d   ≃ _ := ‹step n + d ≃ 0›
  0            ≃ _ := Rel.refl
ℕ : 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
⊢ False
ℕ : 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