have : n * m + m ≃ 0 := calc
  n * m + m  ≃ _ := Rel.symm step_mul
  step n * m ≃ _ := ‹step n * m ≃ 0›
  0          ≃ _ := Rel.refl
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ m ≃ 0
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
⊢ m ≃ 0