Theorem: verus_lemma_mul_strictly_positive (VerusLeanStd/MulInternalsNonlinear.lean)

State before:
x y : ℤ
⊢ 0 < x ∧ 0 < y → 0 < x * y
Tactic:
aesop
State after:
no goals