Theorem: LoVe.BackwardProofs.add_mul (LoVe/Labs/Lab2Solution.lean)

State before:
l m n : ℕ
⊢ mul (add l m) n = add (mul n l) (mul n m)
Tactic:
rw [mul_comm _ n]
State after:
l m n : ℕ
⊢ mul n (add l m) = add (mul n l) (mul n m)

State before:
l m n : ℕ
⊢ mul n (add l m) = add (mul n l) (mul n m)
Tactic:
rw [mul_add]
State after:
no goals