Theorem: verus_lemma_mul_distributes (VerusLeanStd/MulInternals.lean)

State before:
⊢ (∀ (x y z : ℤ), (x + y) * z = x * z + y * z) ∧ ∀ (x y z : ℤ), (x - y) * z = x * z - y * z
Tactic:
exact ⟨Int.add_mul, Int.sub_mul⟩
State after:
no goals