Theorem: MyNat.add_add_add (IIScExperiments/Solutions/NatAddMulExperiments.lean)

State before:
a b c d : MyNat
⊢ a + b + (c + d) = a + c + (b + d)
Tactic:
rw [add_assoc, ← add_assoc b, add_comm b, add_assoc c, ← add_assoc a]
State after:
no goals