Theorem: verus_lemma_mul_nonzero (VerusLeanStd/MulInternalsNonlinear.lean)

State before:
x y : ℤ
⊢ x * y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
Tactic:
aesop
State after:
no goals