Lemmas about subtraction in an unbundled canonically ordered monoids

@[simp]

theorem add_tsub_cancel_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} (h : a ≤ b) : a + (b - a) = b

theorem tsub_add_cancel_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} (h : a ≤ b) : b - a + a = b

theorem add_le_of_le_tsub_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : b ≤ c) (h2 : a ≤ c - b) : a + b ≤ c

theorem add_le_of_le_tsub_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : a ≤ c) (h2 : b ≤ c - a) : a + b ≤ c

theorem tsub_le_tsub_iff_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : c ≤ b) : a - c ≤ b - c ↔ a ≤ b

theorem tsub_left_inj {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h1 : c ≤ a) (h2 : c ≤ b) : a - c = b - c ↔ a = b

theorem tsub_inj_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h₁ : a ≤ b) (h₂ : a ≤ c) : b - a = c - a → b = c

theorem lt_of_tsub_lt_tsub_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : c ≤ b) (h2 : a - c < b - c) : a < b

See lt_of_tsub_lt_tsub_right for a stronger statement in a linear order.

theorem tsub_add_tsub_cancel {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

theorem tsub_tsub_tsub_cancel_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (h : c ≤ b) : a - c - (b - c) = a - b

Lemmas that assume that an element is AddLECancellable.

theorem AddLECancellable.eq_tsub_iff_add_eq_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ b) : a = b - c ↔ a + c = b

theorem AddLECancellable.tsub_eq_iff_eq_add_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : b ≤ a) : a - b = c ↔ a = c + b

theorem AddLECancellable.add_tsub_assoc_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ b) (a : α) : a + b - c = a + (b - c)

theorem AddLECancellable.tsub_add_eq_add_tsub {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (h : b ≤ a) : a - b + c = a + c - b

theorem AddLECancellable.tsub_tsub_assoc {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c

theorem AddLECancellable.tsub_add_tsub_comm {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} {d : α} (hb : AddLECancellable b) (hd : AddLECancellable d) (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)

theorem AddLECancellable.le_tsub_iff_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c

theorem AddLECancellable.le_tsub_iff_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c

theorem AddLECancellable.tsub_lt_iff_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < b + c

theorem AddLECancellable.tsub_lt_iff_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (hba : b ≤ a) : a - b < c ↔ a < c + b

theorem AddLECancellable.tsub_lt_iff_tsub_lt {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hb : AddLECancellable b) (hc : AddLECancellable c) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b

theorem AddLECancellable.le_tsub_iff_le_tsub {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (ha : AddLECancellable a) (hc : AddLECancellable c) (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a

theorem AddLECancellable.lt_tsub_iff_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ a + c < b

theorem AddLECancellable.lt_tsub_iff_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ c + a < b

theorem AddLECancellable.tsub_inj_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c

theorem AddLECancellable.lt_of_tsub_lt_tsub_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (hb : AddLECancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b

theorem AddLECancellable.tsub_lt_tsub_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h : c < b) : a - b < a - c

theorem AddLECancellable.tsub_lt_tsub_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hc : AddLECancellable c) (h : c ≤ a) (h2 : a < b) : a - c < b - c

theorem AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (hb : AddLECancellable b) (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b

@[simp]

theorem AddLECancellable.add_tsub_tsub_cancel {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hac : AddLECancellable (a - c)) (h : c ≤ a) : a + b - (a - c) = b + c

theorem AddLECancellable.tsub_tsub_cancel_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} (hba : AddLECancellable (b - a)) (h : a ≤ b) : b - (b - a) = a

theorem AddLECancellable.tsub_tsub_tsub_cancel_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} (hab : AddLECancellable (a - b)) (h : b ≤ a) : a - c - (a - b) = b - c

Lemmas where addition is order-reflecting.

theorem eq_tsub_iff_add_eq_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ b) : a = b - c ↔ a + c = b

theorem tsub_eq_iff_eq_add_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : b ≤ a) : a - b = c ↔ a = c + b

theorem add_tsub_assoc_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ b) (a : α) : a + b - c = a + (b - c)

See add_tsub_le_assoc for an inequality.

theorem tsub_add_eq_add_tsub {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : b ≤ a) : a - b + c = a + c - b

theorem tsub_tsub_assoc {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c

theorem tsub_add_tsub_comm {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} {d : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)

theorem le_tsub_iff_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a ≤ c) : b ≤ c - a ↔ a + b ≤ c

theorem le_tsub_iff_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a ≤ c) : b ≤ c - a ↔ b + a ≤ c

theorem tsub_lt_iff_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hbc : b ≤ a) : a - b < c ↔ a < b + c

theorem tsub_lt_iff_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (hbc : b ≤ a) : a - b < c ↔ a < c + b

theorem tsub_lt_iff_tsub_lt {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b

theorem le_tsub_iff_le_tsub {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h₁ : a ≤ b) (h₂ : c ≤ b) : a ≤ b - c ↔ c ≤ b - a

theorem lt_tsub_iff_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ b) : a < b - c ↔ a + c < b

See lt_tsub_iff_right for a stronger statement in a linear order.

theorem lt_tsub_iff_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ b) : a < b - c ↔ c + a < b

See lt_tsub_iff_left for a stronger statement in a linear order.

theorem lt_of_tsub_lt_tsub_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (hca : c ≤ a) (h : a - b < a - c) : c < b

See lt_of_tsub_lt_tsub_left for a stronger statement in a linear order.

theorem tsub_lt_tsub_left_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : b ≤ a → c < b → a - b < a - c

theorem tsub_lt_tsub_right_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ a) (h2 : a < b) : a - c < b - c

theorem tsub_inj_right {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h₁ : b ≤ a) (h₂ : c ≤ a) (h₃ : a - b = a - c) : b = c

theorem tsub_lt_tsub_iff_left_of_le_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b

See tsub_lt_tsub_iff_left_of_le for a stronger statement in a linear order.

@[simp]

theorem add_tsub_tsub_cancel {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ a) : a + b - (a - c) = b + c

theorem tsub_tsub_cancel_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : a ≤ b) : b - (b - a) = a

See tsub_tsub_le for an inequality.

theorem tsub_tsub_tsub_cancel_left {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : b ≤ a) : a - c - (a - b) = b - c

theorem tsub_tsub_eq_add_tsub_of_le {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (h : c ≤ b) : a - (b - c) = a + c - b

The tsub version of sub_sub_eq_add_sub.