case h.e'_2.h.e'_5
α : 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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
α : 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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c
convert tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
no goals
case h.e'_2.h.e'_5
α : 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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
rw [tsub_tsub, add_tsub_cancel_of_le hcb]