theorem Lean.Grind.Field.IsOrdered.pos_of_inv_pos {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} (h : 0 < a⁻¹) : 0 < a

theorem Lean.Grind.Field.IsOrdered.inv_pos_iff {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} : 0 < a⁻¹ ↔ 0 < a

theorem Lean.Grind.Field.IsOrdered.inv_neg_iff {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} : a⁻¹ < 0 ↔ a < 0

theorem Lean.Grind.Field.IsOrdered.inv_nonneg_iff {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} : 0 ≤ a⁻¹ ↔ 0 ≤ a

theorem Lean.Grind.Field.IsOrdered.inv_nonpos_iff {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a : R} : a⁻¹ ≤ 0 ↔ a ≤ 0

theorem Lean.Grind.Field.IsOrdered.le_mul_inv_iff_mul_le {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a b : R) {c : R} (h : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b

theorem Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_mul_lt {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a b : R) {c : R} (h : 0 < c) : a < b * c⁻¹ ↔ a * c < b

theorem Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_lt_mul {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b

theorem Lean.Grind.Field.IsOrdered.le_mul_inv_iff_le_mul_of_neg {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a b : R) {c : R} (h : c < 0) : a ≤ b * c⁻¹ ↔ b ≤ a * c

theorem Lean.Grind.Field.IsOrdered.mul_inv_le_iff_mul_le_of_neg {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a c : R) {b : R} (h : b < 0) : a * b⁻¹ ≤ c ↔ c * b ≤ a

theorem Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_lt_mul_of_neg {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a b : R) {c : R} (h : c < 0) : a < b * c⁻¹ ↔ b < a * c

theorem Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_mul_lt_of_neg {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] (a c : R) {b : R} (h : b < 0) : a * b⁻¹ < c ↔ c * b < a

theorem Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_right {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : 0 < c) : a * c < b * c ↔ a < b

theorem Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_pos_left {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : 0 < c) : c * a < c * b ↔ a < b

theorem Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_right {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a

theorem Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_left {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a

theorem Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : 0 < c) : a * c ≤ b * c ↔ a ≤ b

theorem Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_left {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : 0 < c) : c * a ≤ c * b ↔ a ≤ b

theorem Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_right {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a

theorem Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_neg_left {R : Type u} [Field R] [LE R] [LT R] [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [OrderedRing R] {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a