no goals
α : Type u_1
β : Type ?u.33907
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b - c = a - c - b
rw [←tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]