case zero =>
  intro (_ : 0 * m ≃ 0)
  show 0 ≃ 0 ∨ m ≃ 0
  exact Or.inl Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0
no goals