exact mul_preserves_nonzero ‹Nonzero a› ‹Nonzero b›
case h.right
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a * b ≃ 0
this✝¹ : a ≃ 0 ∨ Nonzero a
h✝¹ : Nonzero a
this✝ : b ≃ 0 ∨ Nonzero b
h✝ : Nonzero b
this : ¬(a * b ≃ 0 ∧ Nonzero (a * b))
⊢ Nonzero (a * b)
no goals