no goals
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)
rw [add_assoc, add_tsub_cancel_of_le h, add_comm]