Theorem: IMOSL.Extra.CharTwo.add_comm (IMOSLLean4/Extra/CharTwo/Defs.lean)

State before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y : M
⊢ x + y = y + x
Tactic:
rw [← add_add_cancel_right (x + y) (y + x),
  add_add_add_cancel_middle, add_self_eq_zero, zero_add]
State after:
no goals