α : 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 : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b
α : 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 : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
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 : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)