Theorem: MyNat.add_left_comm (TheoremProvingLean/inductive_types.lean)

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