Theorem: AbelianGroup.zero_add (LeanCourse/Lectures/Lecture8Before.lean)

State before:
n : ℕ
g : AbelianGroup
x : g.G
⊢ add g g.zero x = x
Tactic:
rw [g.comm, g.add_zero]
State after:
no goals