Theorem: verus_lemma_mul_is_associative (VerusLeanStd/MulInternalsNonlinear.lean)

State before:
x y z : ℤ
⊢ x * (y * z) = x * y * z
Tactic:
rw [Int.mul_assoc]
State after:
no goals