α : Type u_1
β : Type ?u.13993
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c ≤ c - b + (a + (b - a))
α : Type u_1
β : Type ?u.13993
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c - a - (c - b) ≤ b - a
rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm]
no goals
α : Type u_1
β : Type ?u.13993
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c ≤ c - b + (a + (b - a))
exact le_tsub_add.trans (add_le_add_left le_add_tsub _)