Theorem: verus_lemma_mul_successor (VerusLeanStd/MulInternals.lean)

State before:
⊢ (∀ (x y : ℤ), (x + 1) * y = x * y + y) ∧ ∀ (x y : ℤ), (x - 1) * y = x * y - y
Tactic:
exact ⟨add_one_mul, sub_one_mul⟩
State after:
no goals