Ordered groups

This file develops the basics of unbundled ordered groups.

Implementation details

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

@[simp]

theorem Left.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : -a ≤ 0 ↔ 0 ≤ a

Uses left co(ntra)variant.

@[simp]

theorem Left.inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses left co(ntra)variant.

@[simp]

theorem Left.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 0 ≤ -a ↔ a ≤ 0

Uses left co(ntra)variant.

@[simp]

theorem Left.one_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Uses left co(ntra)variant.

@[simp]

theorem le_neg_add_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ -a + c ↔ a + b ≤ c

@[simp]

theorem le_inv_mul_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ a⁻¹ * c ↔ a * b ≤ c

@[simp]

theorem neg_add_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : -b + a ≤ c ↔ a ≤ b + c

@[simp]

theorem inv_mul_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b⁻¹ * a ≤ c ↔ a ≤ b * c

theorem neg_le_iff_add_nonneg' {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : -a ≤ b ↔ 0 ≤ a + b

theorem inv_le_iff_one_le_mul' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a⁻¹ ≤ b ↔ 1 ≤ a * b

theorem le_neg_iff_add_nonpos_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ -b ↔ b + a ≤ 0

theorem le_inv_iff_mul_le_one_left {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b⁻¹ ↔ b * a ≤ 1

theorem le_neg_add_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 0 ≤ -b + a ↔ b ≤ a

theorem le_inv_mul_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 1 ≤ b⁻¹ * a ↔ b ≤ a

theorem neg_add_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : -a + b ≤ 0 ↔ b ≤ a

theorem inv_mul_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a⁻¹ * b ≤ 1 ↔ b ≤ a

@[simp]

theorem Left.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 0 < -a ↔ a < 0

Uses left co(ntra)variant.

@[simp]

theorem Left.one_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 1 < a⁻¹ ↔ a < 1

Uses left co(ntra)variant.

@[simp]

theorem Left.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : -a < 0 ↔ 0 < a

Uses left co(ntra)variant.

@[simp]

theorem Left.inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a⁻¹ < 1 ↔ 1 < a

Uses left co(ntra)variant.

@[simp]

theorem lt_neg_add_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < -a + c ↔ a + b < c

@[simp]

theorem lt_inv_mul_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < a⁻¹ * c ↔ a * b < c

@[simp]

theorem neg_add_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -b + a < c ↔ a < b + c

@[simp]

theorem inv_mul_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b⁻¹ * a < c ↔ a < b * c

theorem neg_lt_iff_pos_add' {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : -a < b ↔ 0 < a + b

theorem inv_lt_iff_one_lt_mul' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a⁻¹ < b ↔ 1 < a * b

theorem lt_neg_iff_add_neg' {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a < -b ↔ b + a < 0

theorem lt_inv_iff_mul_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a < b⁻¹ ↔ b * a < 1

theorem lt_neg_add_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 0 < -b + a ↔ b < a

theorem lt_inv_mul_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 1 < b⁻¹ * a ↔ b < a

theorem neg_add_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : -a + b < 0 ↔ b < a

theorem inv_mul_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a⁻¹ * b < 1 ↔ b < a

@[simp]

theorem Right.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : -a ≤ 0 ↔ 0 ≤ a

Uses right co(ntra)variant.

@[simp]

theorem Right.inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Uses right co(ntra)variant.

@[simp]

theorem Right.nonneg_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 0 ≤ -a ↔ a ≤ 0

Uses right co(ntra)variant.

@[simp]

theorem Right.one_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Uses right co(ntra)variant.

theorem neg_le_iff_add_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : -a ≤ b ↔ 0 ≤ b + a

theorem inv_le_iff_one_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a⁻¹ ≤ b ↔ 1 ≤ b * a

theorem le_neg_iff_add_nonpos_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ -b ↔ a + b ≤ 0

theorem le_inv_iff_mul_le_one_right {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b⁻¹ ↔ a * b ≤ 1

@[simp]

theorem add_neg_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a + -b ≤ c ↔ a ≤ c + b

@[simp]

theorem mul_inv_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a * b⁻¹ ≤ c ↔ a ≤ c * b

@[simp]

theorem le_add_neg_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : c ≤ a + -b ↔ c + b ≤ a

@[simp]

theorem le_mul_inv_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : c ≤ a * b⁻¹ ↔ c * b ≤ a

theorem add_neg_nonpos_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a + -b ≤ 0 ↔ a ≤ b

theorem mul_inv_le_one_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a * b⁻¹ ≤ 1 ↔ a ≤ b

theorem le_add_neg_iff_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 0 ≤ a + -b ↔ b ≤ a

theorem le_mul_inv_iff_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 1 ≤ a * b⁻¹ ↔ b ≤ a

theorem add_neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : b + -a ≤ 0 ↔ b ≤ a

theorem mul_inv_le_one_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : b * a⁻¹ ≤ 1 ↔ b ≤ a

@[simp]

theorem Right.neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : -a < 0 ↔ 0 < a

Uses right co(ntra)variant.

@[simp]

theorem Right.inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a⁻¹ < 1 ↔ 1 < a

Uses right co(ntra)variant.

@[simp]

theorem Right.neg_pos_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 0 < -a ↔ a < 0

Uses right co(ntra)variant.

@[simp]

theorem Right.one_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 1 < a⁻¹ ↔ a < 1

Uses right co(ntra)variant.

theorem neg_lt_iff_pos_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : -a < b ↔ 0 < b + a

theorem inv_lt_iff_one_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a⁻¹ < b ↔ 1 < b * a

theorem lt_neg_iff_add_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a < -b ↔ a + b < 0

theorem lt_inv_iff_mul_lt_one {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a < b⁻¹ ↔ a * b < 1

@[simp]

theorem add_neg_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a + -b < c ↔ a < c + b

@[simp]

theorem mul_inv_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a * b⁻¹ < c ↔ a < c * b

@[simp]

theorem lt_add_neg_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : c < a + -b ↔ c + b < a

@[simp]

theorem lt_mul_inv_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : c < a * b⁻¹ ↔ c * b < a

theorem neg_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a + -b < 0 ↔ a < b

theorem inv_mul_lt_one_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a * b⁻¹ < 1 ↔ a < b

theorem lt_add_neg_iff_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 0 < a + -b ↔ b < a

theorem lt_mul_inv_iff_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 1 < a * b⁻¹ ↔ b < a

theorem add_neg_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : b + -a < 0 ↔ b < a

theorem mul_inv_lt_one_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : b * a⁻¹ < 1 ↔ b < a

@[simp]

theorem sub_le_self_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b

@[simp]

theorem div_le_self_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b

@[simp]

theorem le_sub_self_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) {b : α} : a ≤ a - b ↔ b ≤ 0

@[simp]

theorem le_div_self_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1

theorem sub_le_self {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) {b : α} : 0 ≤ b → a - b ≤ a

Alias of the reverse direction of sub_le_self_iff.

@[simp]

theorem neg_le_neg_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : -a ≤ -b ↔ b ≤ a

@[simp]

theorem inv_le_inv_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

theorem le_of_neg_le_neg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : -a ≤ -b → b ≤ a

Alias of the forward direction of neg_le_neg_iff.

theorem add_neg_le_neg_add_iff {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a + -b ≤ -d + c ↔ d + a ≤ c + b

theorem mul_inv_le_inv_mul_iff {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

@[simp]

theorem sub_lt_self_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} : a - b < a ↔ 0 < b

@[simp]

theorem div_lt_self_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} : a / b < a ↔ 1 < b

theorem sub_lt_self {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] (a : α) {b : α} : 0 < b → a - b < a

Alias of the reverse direction of sub_lt_self_iff.

@[simp]

theorem neg_lt_neg_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : -a < -b ↔ b < a

@[simp]

theorem inv_lt_inv_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a⁻¹ < b⁻¹ ↔ b < a

theorem neg_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : -a < b ↔ -b < a

theorem inv_lt' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a⁻¹ < b ↔ b⁻¹ < a

theorem lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : a < -b ↔ b < -a

theorem lt_inv' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a < b⁻¹ ↔ b < a⁻¹

theorem lt_inv_of_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a < b⁻¹ → b < a⁻¹

Alias of the forward direction of lt_inv'.

theorem lt_neg_of_lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : a < -b → b < -a

theorem inv_lt_of_inv_lt' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a⁻¹ < b → b⁻¹ < a

Alias of the forward direction of inv_lt'.

theorem neg_lt_of_neg_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : -a < b → -b < a

theorem add_neg_lt_neg_add_iff {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : a + -b < -d + c ↔ d + a < c + b

theorem mul_inv_lt_inv_mul_iff {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b

theorem Left.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : 0 ≤ a) : -a ≤ a

theorem Left.inv_le_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a

theorem neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : 0 ≤ a) : -a ≤ a

Alias of Left.neg_le_self.

theorem Left.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : a ≤ 0) : a ≤ -a

theorem Left.self_le_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : a ≤ 1) : a ≤ a⁻¹

theorem Left.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) : -a < a

theorem Left.inv_lt_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 1 < a) : a⁻¹ < a

theorem neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) : -a < a

Alias of Left.neg_lt_self.

theorem Left.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 0) : a < -a

theorem Left.self_lt_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 1) : a < a⁻¹

theorem Right.neg_le_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : 0 ≤ a) : -a ≤ a

theorem Right.inv_le_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : 1 ≤ a) : a⁻¹ ≤ a

theorem Right.self_le_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : a ≤ 0) : a ≤ -a

theorem Right.self_le_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} (h : a ≤ 1) : a ≤ a⁻¹

theorem Right.neg_lt_self {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 0 < a) : -a < a

theorem Right.inv_lt_self {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : 1 < a) : a⁻¹ < a

theorem Right.self_lt_neg {α : Type u} [AddGroup α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 0) : a < -a

theorem Right.self_lt_inv {α : Type u} [Group α] [Preorder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} (h : a < 1) : a < a⁻¹

theorem neg_add_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : -c + a ≤ b ↔ a ≤ b + c

theorem inv_mul_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : c⁻¹ * a ≤ b ↔ a ≤ b * c

theorem add_neg_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a + -b ≤ c ↔ a ≤ b + c

theorem mul_inv_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a * b⁻¹ ≤ c ↔ a ≤ b * c

theorem add_neg_le_add_neg_iff {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a + -b ≤ c + -d ↔ a + d ≤ c + b

theorem mul_inv_le_mul_inv_iff' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

theorem neg_add_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -c + a < b ↔ a < b + c

theorem inv_mul_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : c⁻¹ * a < b ↔ a < b * c

theorem add_neg_lt_iff_le_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a + -b < c ↔ a < b + c

theorem mul_inv_lt_iff_le_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a * b⁻¹ < c ↔ a < b * c

theorem add_neg_lt_add_neg_iff {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} : a + -b < c + -d ↔ a + d < c + b

theorem mul_inv_lt_mul_inv_iff' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} : a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b

theorem one_le_of_inv_le_one {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : a⁻¹ ≤ 1 → 1 ≤ a

Alias of the forward direction of Left.inv_le_one_iff.

---

Uses left co(ntra)variant.

theorem nonneg_of_neg_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : -a ≤ 0 → 0 ≤ a

theorem le_one_of_one_le_inv {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 1 ≤ a⁻¹ → a ≤ 1

Alias of the forward direction of Left.one_le_inv_iff.

---

Uses left co(ntra)variant.

theorem nonpos_of_neg_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 0 ≤ -a → a ≤ 0

theorem lt_of_inv_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : a⁻¹ < b⁻¹ → b < a

Alias of the forward direction of inv_lt_inv_iff.

theorem lt_of_neg_lt_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : -a < -b → b < a

theorem one_lt_of_inv_lt_one {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a⁻¹ < 1 → 1 < a

Alias of the forward direction of Left.inv_lt_one_iff.

---

Uses left co(ntra)variant.

theorem pos_of_neg_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : -a < 0 → 0 < a

theorem inv_lt_one_iff_one_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a⁻¹ < 1 ↔ 1 < a

Alias of Left.inv_lt_one_iff.

---

Uses left co(ntra)variant.

theorem neg_neg_iff_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : -a < 0 ↔ 0 < a

theorem inv_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a⁻¹ < 1 ↔ 1 < a

Alias of Left.inv_lt_one_iff.

---

Uses left co(ntra)variant.

theorem neg_lt_zero {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : -a < 0 ↔ 0 < a

theorem inv_of_one_lt_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 1 < a⁻¹ → a < 1

Alias of the forward direction of Left.one_lt_inv_iff.

---

Uses left co(ntra)variant.

theorem neg_of_neg_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 0 < -a → a < 0

theorem one_lt_inv_of_inv {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a < 1 → 1 < a⁻¹

Alias of the reverse direction of Left.one_lt_inv_iff.

---

Uses left co(ntra)variant.

theorem neg_pos_of_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : a < 0 → 0 < -a

theorem mul_le_of_le_inv_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ a⁻¹ * c → a * b ≤ c

Alias of the forward direction of le_inv_mul_iff_mul_le.

theorem add_le_of_le_neg_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ -a + c → a + b ≤ c

theorem le_inv_mul_of_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a * b ≤ c → b ≤ a⁻¹ * c

Alias of the reverse direction of le_inv_mul_iff_mul_le.

theorem le_neg_add_of_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a + b ≤ c → b ≤ -a + c

theorem inv_mul_le_of_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ b * c → b⁻¹ * a ≤ c

Alias of the reverse direction of inv_mul_le_iff_le_mul.

theorem neg_add_le_of_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ b + c → -b + a ≤ c

theorem mul_lt_of_lt_inv_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < a⁻¹ * c → a * b < c

Alias of the forward direction of lt_inv_mul_iff_mul_lt.

theorem add_lt_of_lt_neg_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < -a + c → a + b < c

theorem lt_inv_mul_of_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a * b < c → b < a⁻¹ * c

Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

theorem lt_neg_add_of_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a + b < c → b < -a + c

theorem lt_mul_of_inv_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b⁻¹ * a < c → a < b * c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

theorem inv_mul_lt_of_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b * c → b⁻¹ * a < c

Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

theorem lt_add_of_neg_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -b + a < c → a < b + c

theorem neg_add_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b + c → -b + a < c

theorem lt_mul_of_inv_mul_lt_left {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b⁻¹ * a < c → a < b * c

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

---

Alias of the forward direction of inv_mul_lt_iff_lt_mul.

theorem lt_add_of_neg_add_lt_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -b + a < c → a < b + c

theorem inv_le_one' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : a⁻¹ ≤ 1 ↔ 1 ≤ a

Alias of Left.inv_le_one_iff.

---

Uses left co(ntra)variant.

theorem neg_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : -a ≤ 0 ↔ 0 ≤ a

theorem one_le_inv' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 1 ≤ a⁻¹ ↔ a ≤ 1

Alias of Left.one_le_inv_iff.

---

Uses left co(ntra)variant.

theorem neg_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} : 0 ≤ -a ↔ a ≤ 0

theorem one_lt_inv' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 1 < a⁻¹ ↔ a < 1

Alias of Left.one_lt_inv_iff.

---

Uses left co(ntra)variant.

theorem neg_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} : 0 < -a ↔ a < 0

theorem sub_le_sub_iff_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (c : α) : a - c ≤ b - c ↔ a ≤ b

theorem div_le_div_iff_right {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (c : α) : a / c ≤ b / c ↔ a ≤ b

theorem sub_le_sub_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c

theorem div_le_div_right' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : a ≤ b) (c : α) : a / c ≤ b / c

@[simp]

theorem sub_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 0 ≤ a - b ↔ b ≤ a

@[simp]

theorem one_le_div' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 1 ≤ a / b ↔ b ≤ a

theorem le_of_sub_nonneg {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : 0 ≤ a - b → b ≤ a

Alias of the forward direction of sub_nonneg.

theorem sub_nonneg_of_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : b ≤ a → 0 ≤ a - b

Alias of the reverse direction of sub_nonneg.

theorem sub_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a - b ≤ 0 ↔ a ≤ b

theorem div_le_one' {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a / b ≤ 1 ↔ a ≤ b

theorem le_of_sub_nonpos {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a - b ≤ 0 → a ≤ b

Alias of the forward direction of sub_nonpos.

theorem sub_nonpos_of_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b → a - b ≤ 0

Alias of the reverse direction of sub_nonpos.

theorem le_sub_iff_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ c - b ↔ a + b ≤ c

theorem le_div_iff_mul_le {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ c / b ↔ a * b ≤ c

theorem add_le_of_le_sub_right {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ c - b → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le.

theorem le_sub_right_of_add_le {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a + b ≤ c → a ≤ c - b

Alias of the reverse direction of le_sub_iff_add_le.

theorem sub_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a - c ≤ b ↔ a ≤ b + c

@[simp]

theorem div_le_iff_le_mul {α : Type u} [Group α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a / c ≤ b ↔ a ≤ b * c

@[instance 100]

instance AddGroup.toOrderedSub {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : OrderedSub α

Equations

• ⋯ = ⋯

theorem sub_le_sub_iff_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {b : α} {c : α} (a : α) : a - b ≤ a - c ↔ c ≤ b

theorem div_le_div_iff_left {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {b : α} {c : α} (a : α) : a / b ≤ a / c ↔ c ≤ b

theorem sub_le_sub_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : a ≤ b) (c : α) : c - b ≤ c - a

theorem div_le_div_left' {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : a ≤ b) (c : α) : c / b ≤ c / a

theorem sub_le_sub_iff {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a - b ≤ c - d ↔ a + d ≤ c + b

theorem div_le_div_iff' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a / b ≤ c / d ↔ a * d ≤ c * b

theorem le_sub_iff_add_le' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ c - a ↔ a + b ≤ c

theorem le_div_iff_mul_le' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ c / a ↔ a * b ≤ c

theorem add_le_of_le_sub_left {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b ≤ c - a → a + b ≤ c

Alias of the forward direction of le_sub_iff_add_le'.

theorem le_sub_left_of_add_le {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a + b ≤ c → b ≤ c - a

Alias of the reverse direction of le_sub_iff_add_le'.

theorem sub_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a ≤ b + c

theorem div_le_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a / b ≤ c ↔ a ≤ b * c

theorem sub_left_le_of_le_add {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ b + c → a - b ≤ c

Alias of the reverse direction of sub_le_iff_le_add'.

theorem le_add_of_sub_left_le {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a - b ≤ c → a ≤ b + c

Alias of the forward direction of sub_le_iff_le_add'.

@[simp]

theorem neg_le_sub_iff_le_add {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : -b ≤ a - c ↔ c ≤ a + b

@[simp]

theorem inv_le_div_iff_le_mul {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : b⁻¹ ≤ a / c ↔ c ≤ a * b

theorem neg_le_sub_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : -a ≤ b - c ↔ c ≤ a + b

theorem inv_le_div_iff_le_mul' {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a⁻¹ ≤ b / c ↔ c ≤ a * b

theorem sub_le_comm {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a - b ≤ c ↔ a - c ≤ b

theorem div_le_comm {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a / b ≤ c ↔ a / c ≤ b

theorem le_sub_comm {α : Type u} [AddCommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ b - c ↔ c ≤ b - a

theorem le_div_comm {α : Type u} [CommGroup α] [LE α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} : a ≤ b / c ↔ c ≤ b / a

theorem sub_le_sub {α : Type u} [AddCommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c

theorem div_le_div'' {α : Type u} [CommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c

@[simp]

theorem sub_lt_sub_iff_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (c : α) : a - c < b - c ↔ a < b

@[simp]

theorem div_lt_div_iff_right {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (c : α) : a / c < b / c ↔ a < b

theorem sub_lt_sub_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) : a - c < b - c

theorem div_lt_div_right' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) : a / c < b / c

@[simp]

theorem sub_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 0 < a - b ↔ b < a

@[simp]

theorem one_lt_div' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 1 < a / b ↔ b < a

theorem sub_pos_of_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : b < a → 0 < a - b

Alias of the reverse direction of sub_pos.

theorem lt_of_sub_pos {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : 0 < a - b → b < a

Alias of the forward direction of sub_pos.

@[simp]

theorem sub_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a - b < 0 ↔ a < b

For a - -b = a + b, see sub_neg_eq_add.

@[simp]

theorem div_lt_one' {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a / b < 1 ↔ a < b

theorem lt_of_sub_neg {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a - b < 0 → a < b

Alias of the forward direction of sub_neg.

---

For a - -b = a + b, see sub_neg_eq_add.

theorem sub_neg_of_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a < b → a - b < 0

Alias of the reverse direction of sub_neg.

---

For a - -b = a + b, see sub_neg_eq_add.

theorem sub_lt_zero {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} : a - b < 0 ↔ a < b

Alias of sub_neg.

---

For a - -b = a + b, see sub_neg_eq_add.

theorem lt_sub_iff_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < c - b ↔ a + b < c

theorem lt_div_iff_mul_lt {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < c / b ↔ a * b < c

theorem add_lt_of_lt_sub_right {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < c - b → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt.

theorem lt_sub_right_of_add_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a + b < c → a < c - b

Alias of the reverse direction of lt_sub_iff_add_lt.

theorem sub_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a - c < b ↔ a < b + c

theorem div_lt_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a / c < b ↔ a < b * c

theorem lt_add_of_sub_right_lt {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a - c < b → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add.

theorem sub_right_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b + c → a - c < b

Alias of the reverse direction of sub_lt_iff_lt_add.

@[simp]

theorem sub_lt_sub_iff_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {b : α} {c : α} (a : α) : a - b < a - c ↔ c < b

@[simp]

theorem div_lt_div_iff_left {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {b : α} {c : α} (a : α) : a / b < a / c ↔ c < b

@[simp]

theorem neg_lt_sub_iff_lt_add {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -a < b - c ↔ c < a + b

@[simp]

theorem inv_lt_div_iff_lt_mul {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a⁻¹ < b / c ↔ c < a * b

theorem sub_lt_sub_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) : c - b < c - a

theorem div_lt_div_left' {α : Type u} [Group α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) (c : α) : c / b < c / a

theorem sub_lt_sub_iff {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} : a - b < c - d ↔ a + d < c + b

theorem div_lt_div_iff' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} : a / b < c / d ↔ a * d < c * b

theorem lt_sub_iff_add_lt' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < c - a ↔ a + b < c

theorem lt_div_iff_mul_lt' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < c / a ↔ a * b < c

theorem lt_sub_left_of_add_lt {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a + b < c → b < c - a

Alias of the reverse direction of lt_sub_iff_add_lt'.

theorem add_lt_of_lt_sub_left {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b < c - a → a + b < c

Alias of the forward direction of lt_sub_iff_add_lt'.

theorem sub_lt_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a - b < c ↔ a < b + c

theorem div_lt_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a / b < c ↔ a < b * c

theorem sub_left_lt_of_lt_add {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b + c → a - b < c

Alias of the reverse direction of sub_lt_iff_lt_add'.

theorem lt_add_of_sub_left_lt {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a - b < c → a < b + c

Alias of the forward direction of sub_lt_iff_lt_add'.

theorem neg_lt_sub_iff_lt_add' {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : -b < a - c ↔ c < a + b

theorem inv_lt_div_iff_lt_mul' {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : b⁻¹ < a / c ↔ c < a * b

theorem sub_lt_comm {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a - b < c ↔ a - c < b

theorem div_lt_comm {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a / b < c ↔ a / c < b

theorem lt_sub_comm {α : Type u} [AddCommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b - c ↔ c < b - a

theorem lt_div_comm {α : Type u} [CommGroup α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} : a < b / c ↔ c < b / a

theorem sub_lt_sub {α : Type u} [AddCommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) : a - d < b - c

theorem div_lt_div'' {α : Type u} [CommGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) : a / d < b / c

theorem lt_or_lt_of_sub_lt_sub {α : Type u} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a - d < b - c → a < b ∨ c < d

theorem lt_or_lt_of_div_lt_div {α : Type u} [CommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} {c : α} {d : α} : a / d < b / c → a < b ∨ c < d

@[simp]

theorem cmp_sub_zero {α : Type u} [AddGroup α] [LinearOrder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : cmp (a - b) 0 = cmp a b

@[simp]

theorem cmp_div_one' {α : Type u} [Group α] [LinearOrder α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : cmp (a / b) 1 = cmp a b

theorem le_of_forall_pos_lt_add {α : Type u} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) : a ≤ b

theorem le_of_forall_one_lt_lt_mul {α : Type u} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (h : ∀ (ε : α), 1 < ε → a < b * ε) : a ≤ b

theorem le_iff_forall_pos_lt_add {α : Type u} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε

theorem le_iff_forall_one_lt_lt_mul {α : Type u} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε

theorem sub_le_neg_add_iff {α : Type u} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : a - b ≤ -a + b ↔ a ≤ b

theorem div_le_inv_mul_iff {α : Type u} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : a / b ≤ a⁻¹ * b ↔ a ≤ b

theorem sub_le_sub_flip {α : Type u_1} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a - b ≤ b - a ↔ a ≤ b

theorem div_le_div_flip {α : Type u_1} [CommGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} : a / b ≤ b / a ↔ a ≤ b

theorem Monotone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun (x : β) => -f x

theorem Monotone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} (hf : Monotone f) : Antitone fun (x : β) => (f x)⁻¹

theorem Antitone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun (x : β) => -f x

theorem Antitone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} (hf : Antitone f) : Monotone fun (x : β) => (f x)⁻¹

theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun (x : β) => -f x) s

theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} {s : Set β} (hf : MonotoneOn f s) : AntitoneOn (fun (x : β) => (f x)⁻¹) s

theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun (x : β) => -f x) s

theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [Preorder β] {f : β → α} {s : Set β} (hf : AntitoneOn f s) : MonotoneOn (fun (x : β) => (f x)⁻¹) s

theorem StrictMono.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun (x : β) => -f x

theorem StrictMono.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} (hf : StrictMono f) : StrictAnti fun (x : β) => (f x)⁻¹

theorem StrictAnti.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun (x : β) => -f x

theorem StrictAnti.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} (hf : StrictAnti f) : StrictMono fun (x : β) => (f x)⁻¹

theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun (x : β) => -f x) s

theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} {s : Set β} (hf : StrictMonoOn f s) : StrictAntiOn (fun (x : β) => (f x)⁻¹) s

theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun (x : β) => -f x) s

theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [Preorder β] {f : β → α} {s : Set β} (hf : StrictAntiOn f s) : StrictMonoOn (fun (x : β) => (f x)⁻¹) s