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

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