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

State before:
G : Type u_1
inst✝¹ : AddGroup G
inst✝ : CharTwo G
x y : G
⊢ x - y = x + y
Tactic:
rw [sub_eq_add_neg, neg_eq_self]
State after:
no goals