# Lemmas about subtraction in canonically ordered monoids #

@[simp]
theorem add_tsub_cancel_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} (h : a b) :
a + (b - a) = b
theorem tsub_add_cancel_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} (h : a b) :
b - a + a = b
theorem add_le_of_le_tsub_right_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (h : a c) (h2 : b c - a) :
a + b c
theorem tsub_le_tsub_iff_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (h : c b) :
a - c b - c a b
theorem tsub_left_inj {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (h1 : c a) (h2 : c b) :
a - c = b - c a = b
theorem tsub_inj_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : a c) :
b - a = c - ab = c
theorem lt_of_tsub_lt_tsub_right_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hab : b a) (hcb : c b) :
a - b + (b - c) = a - c
theorem tsub_tsub_tsub_cancel_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hc : ) (h : c b) :
a = b - c a + c = b
theorem AddLECancellable.tsub_eq_iff_eq_add_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hb : ) (h : b a) :
a - b = c a = c + b
theorem AddLECancellable.add_tsub_assoc_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {b : α} {c : α} (hc : ) (h : c b) (a : α) :
a + b - c = a + (b - c)
theorem AddLECancellable.tsub_add_eq_add_tsub {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hb : ) (h : b a) :
a - b + c = a + c - b
theorem AddLECancellable.tsub_tsub_assoc {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} {d : α} (hb : ) (hd : ) (hba : b a) (hdc : d c) :
a - b + (c - d) = a + c - (b + d)
theorem AddLECancellable.le_tsub_iff_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (h : a c) :
b c - a a + b c
theorem AddLECancellable.le_tsub_iff_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (h : a c) :
b c - a b + a c
theorem AddLECancellable.tsub_lt_iff_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hb : ) (hba : b a) :
a - b < c a < b + c
theorem AddLECancellable.tsub_lt_iff_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hb : ) (hba : b a) :
a - b < c a < c + b
theorem AddLECancellable.tsub_lt_iff_tsub_lt {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hb : ) (hc : ) (h₁ : b a) (h₂ : c a) :
a - b < c a - c < b
theorem AddLECancellable.le_tsub_iff_le_tsub {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (hc : ) (h₁ : a b) (h₂ : c b) :
a b - c c b - a
theorem AddLECancellable.lt_tsub_iff_right_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hc : ) (h : c b) :
a < b - c a + c < b
theorem AddLECancellable.lt_tsub_iff_left_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hc : ) (h : c b) :
a < b - c c + a < b
theorem AddLECancellable.tsub_inj_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (hb : ) (hca : c a) (h : a - b < a - c) :
c < b
theorem AddLECancellable.tsub_lt_tsub_left_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} (hc : ) (h : c a) (h2 : a < b) :
a - c < b - c
theorem AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (hb : ) (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} (hba : AddLECancellable (b - a)) (h : a b) :
b - (b - a) = a
theorem AddLECancellable.tsub_tsub_tsub_cancel_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c b) :
a = b - c a + c = b
theorem tsub_eq_iff_eq_add_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : b a) :
a - b = c a = c + b
theorem add_tsub_assoc_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : b a) :
a - b + c = a + c - b
theorem tsub_tsub_assoc {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h₁ : b a) (h₂ : c b) :
a - (b - c) = a - b + c
theorem tsub_add_tsub_comm {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} {d : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (hba : b a) (hdc : d c) :
a - b + (c - d) = a + c - (b + d)
theorem le_tsub_iff_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : a c) :
b c - a a + b c
theorem le_tsub_iff_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : a c) :
b c - a b + a c
theorem tsub_lt_iff_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (hbc : b a) :
a - b < c a < b + c
theorem tsub_lt_iff_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (hbc : b a) :
a - b < c a < c + b
theorem tsub_lt_iff_tsub_lt {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h₁ : b a) (h₂ : c a) :
a - b < c a - c < b
theorem le_tsub_iff_le_tsub {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h₁ : a b) (h₂ : c b) :
a b - c c b - a
theorem lt_tsub_iff_right_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
b ac < ba - b < a - c
theorem tsub_lt_tsub_right_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c a) (h2 : a < b) :
a - c < b - c
theorem tsub_inj_right {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] (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} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c a) :
a + b - (a - c) = b + c
theorem tsub_tsub_cancel_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : a b) :
b - (b - a) = a

See tsub_tsub_le for an inequality.

theorem tsub_tsub_tsub_cancel_left {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : b a) :
a - c - (a - b) = b - c
theorem tsub_tsub_eq_add_tsub_of_le {α : Type u_1} [] [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c b) :
a - (b - c) = a + c - b

The tsub version of sub_sub_eq_add_sub.

### Lemmas in a canonically ordered monoid. #

theorem add_tsub_cancel_iff_le {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a + (b - a) = b a b
theorem tsub_add_cancel_iff_le {α : Type u_1} [Sub α] [] {a : α} {b : α} :
b - a + a = b a b
theorem tsub_eq_zero_iff_le {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a - b = 0 a b
@[simp]
theorem tsub_eq_zero_of_le {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a ba - b = 0

Alias of the reverse direction of tsub_eq_zero_iff_le.

theorem tsub_self {α : Type u_1} [Sub α] [] (a : α) :
a - a = 0
theorem tsub_le_self {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a - b a
theorem zero_tsub {α : Type u_1} [Sub α] [] (a : α) :
0 - a = 0
theorem tsub_self_add {α : Type u_1} [Sub α] [] (a : α) (b : α) :
a - (a + b) = 0
theorem tsub_pos_iff_not_le {α : Type u_1} [Sub α] [] {a : α} {b : α} :
0 < a - b ¬a b
theorem tsub_pos_of_lt {α : Type u_1} [Sub α] [] {a : α} {b : α} (h : a < b) :
0 < b - a
theorem tsub_lt_of_lt {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (h : a < b) :
a - c < b
theorem AddLECancellable.tsub_le_tsub_iff_left {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (hc : ) (h : c a) :
a - b a - c c b
theorem AddLECancellable.tsub_right_inj {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (hb : ) (hc : ) (hba : b a) (hca : c a) :
a - b = a - c b = c

#### Lemmas where addition is order-reflecting. #

theorem tsub_le_tsub_iff_left {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c a) :
a - b a - c c b
theorem tsub_right_inj {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (hba : b a) (hca : c a) :
a - b = a - c b = c
@[reducible, inline]
abbrev CanonicallyOrderedAddCommMonoid.toAddCancelCommMonoid (α : Type u_1) [Sub α] [] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :

A CanonicallyOrderedAddCommMonoid with ordered subtraction and order-reflecting addition is cancellative. This is not an instance as it would form a typeclass loop.

See note [reducible non-instances].

Equations
• = let __src := inferInstance;
Instances For

### Lemmas in a linearly canonically ordered monoid. #

@[simp]
theorem tsub_pos_iff_lt {α : Type u_1} [Sub α] [] {a : α} {b : α} :
0 < a - b b < a
theorem tsub_eq_tsub_min {α : Type u_1} [Sub α] [] (a : α) (b : α) :
a - b = a - min a b
theorem AddLECancellable.lt_tsub_iff_right {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (hc : ) :
a < b - c a + c < b
theorem AddLECancellable.lt_tsub_iff_left {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (hc : ) :
a < b - c c + a < b
theorem AddLECancellable.tsub_lt_tsub_iff_right {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (hc : ) (h : c a) :
a - c < b - c a < b
theorem AddLECancellable.tsub_lt_self {α : Type u_1} [Sub α] [] {a : α} {b : α} (ha : ) (h₁ : 0 < a) (h₂ : 0 < b) :
a - b < a
theorem AddLECancellable.tsub_lt_self_iff {α : Type u_1} [Sub α] [] {a : α} {b : α} (ha : ) :
a - b < a 0 < a 0 < b
theorem AddLECancellable.tsub_lt_tsub_iff_left_of_le {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} (ha : ) (hb : ) (h : b a) :
a - b < a - c c < b

See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.

theorem tsub_lt_tsub_iff_right {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : c a) :
a - c < b - c a < b

This lemma also holds for ENNReal, but we need a different proof for that.

theorem tsub_lt_self {α : Type u_1} [Sub α] [] {a : α} {b : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
0 < a0 < ba - b < a
@[simp]
theorem tsub_lt_self_iff {α : Type u_1} [Sub α] [] {a : α} {b : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
a - b < a 0 < a 0 < b
theorem tsub_lt_tsub_iff_left_of_le {α : Type u_1} [Sub α] [] {a : α} {b : α} {c : α} [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : b a) :
a - b < a - c c < b

See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.

theorem tsub_tsub_eq_min {α : Type u_1} [Sub α] [] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a - (a - b) = min a b

### Lemmas about max and min. #

theorem tsub_add_eq_max {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a - b + b = max a b
theorem add_tsub_eq_max {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a + (b - a) = max a b
theorem tsub_min {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a - min a b = a - b
theorem tsub_add_min {α : Type u_1} [Sub α] [] {a : α} {b : α} :
a - b + min a b = a
theorem Even.tsub {α : Type u_1} [Sub α] [] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {m : α} {n : α} (hm : Even m) (hn : Even n) :
Even (m - n)