α : 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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + 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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c
rw [add_comm]
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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c
exact ha.le_tsub_iff_left h