case a
α : Type u_1
β : Type ?u.31044
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c ≤ b - (a + c)

case a
α : Type u_1
β : Type ?u.31044
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - (a + c) ≤ b - a - c
α : Type u_1
β : Type ?u.31044
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c = b - (a + c)
apply le_antisymm
no goals
case a
α : Type u_1
β : Type ?u.31044
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c ≤ b - (a + c)
rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
no goals
case a
α : Type u_1
β : Type ?u.31044
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - (a + c) ≤ b - a - c
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]