Theorem: Point.add_commutative (LeanCourse/Lectures/Lecture8Before.lean)

State before:
n : ℕ
a b : Point
⊢ add a b = add b a
Tactic:
simp [add, add_comm]
State after:
no goals