no goals
α : Type u_1
β : Type ?u.41593
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a + c < b
⊢ c + a < b
rwa [add_comm]