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