exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝¹ m n₂✝ n₂ : ℕ
x✝ : 0 ≃ step n₂
⊢ 0 * m ≃ step n₂ * m
no goals