α : Type u_1
β : Type ?u.12335
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
⊢ a ≤ c + (b - c) + (a - b)
α : Type u_1
β : Type ?u.12335
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
⊢ a - c ≤ a - b + (b - c)
rw [tsub_le_iff_left, ← add_assoc, add_right_comm]
no goals
α : Type u_1
β : Type ?u.12335
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
⊢ a ≤ c + (b - c) + (a - b)
exact le_add_tsub.trans (add_le_add_right le_add_tsub _)