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

State before:
M : Type u_1
inst✝¹ : AddMonoid M
inst✝ : CharTwo M
x y z : M
⊢ x + z = y + z ↔ x = y
Tactic:
rw [add_comm, add_comm y, add_right_inj]
State after:
no goals