no goals
α : Type u_1
β : Type ?u.36062
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = b + c
⊢ a = c + b
rw [add_comm, h]