class Lean.Grind.Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends Lean.Grind.IntModule.IsOrdered R : Prop

• neg_le_iff (a b : R) : -a ≤ b ↔ -b ≤ a
• add_le_left {a b : R} : a ≤ b → ∀ (c : R), a + c ≤ b + c
• hmul_pos (k : Int) {a : R} : 0 < a → (0 < k ↔ 0 < k * a)
• hmul_nonneg {k : Int} {a : R} : 0 ≤ k → 0 ≤ a → 0 ≤ k * a
• zero_lt_one : 0 < 1

  In a strict ordered semiring, we have 0 < 1.

• mul_lt_mul_of_pos_left {a b c : R} : a < b → 0 < c → c * a < c * b

  In a strict ordered semiring, we can multiply an inequality a < b on the left by a positive element 0 < c to obtain c * a < c * b.

• mul_lt_mul_of_pos_right {a b c : R} : a < b → 0 < c → a * c < b * c

  In a strict ordered semiring, we can multiply an inequality a < b on the right by a positive element 0 < c to obtain a * c < b * c.

theorem Lean.Grind.Ring.IsOrdered.zero_le_one {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] : 0 ≤ 1

theorem Lean.Grind.Ring.IsOrdered.not_one_lt_zero {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] : ¬1 < 0

theorem Lean.Grind.Ring.IsOrdered.mul_le_mul_of_nonneg_left {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b

theorem Lean.Grind.Ring.IsOrdered.mul_le_mul_of_nonneg_right {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c

theorem Lean.Grind.Ring.IsOrdered.mul_le_mul_of_nonpos_left {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : c * b ≤ c * a

theorem Lean.Grind.Ring.IsOrdered.mul_le_mul_of_nonpos_right {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : b * c ≤ a * c

theorem Lean.Grind.Ring.IsOrdered.mul_lt_mul_of_neg_left {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a

theorem Lean.Grind.Ring.IsOrdered.mul_lt_mul_of_neg_right {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c

theorem Lean.Grind.Ring.IsOrdered.mul_nonneg {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b

theorem Lean.Grind.Ring.IsOrdered.mul_nonneg_of_nonpos_of_nonpos {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : 0 ≤ a * b

theorem Lean.Grind.Ring.IsOrdered.mul_nonpos_of_nonneg_of_nonpos {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) : a * b ≤ 0

theorem Lean.Grind.Ring.IsOrdered.mul_nonpos_of_nonpos_of_nonneg {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : a ≤ 0) (h₂ : 0 ≤ b) : a * b ≤ 0

theorem Lean.Grind.Ring.IsOrdered.mul_pos {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b

theorem Lean.Grind.Ring.IsOrdered.mul_pos_of_neg_of_neg {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : a < 0) (h₂ : b < 0) : 0 < a * b

theorem Lean.Grind.Ring.IsOrdered.mul_neg_of_pos_of_neg {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : 0 < a) (h₂ : b < 0) : a * b < 0

theorem Lean.Grind.Ring.IsOrdered.mul_neg_of_neg_of_pos {R : Type u} [Ring R] [PartialOrder R] [IsOrdered R] {a b : R} (h₁ : a < 0) (h₂ : 0 < b) : a * b < 0

theorem Lean.Grind.Ring.IsOrdered.mul_nonneg_iff {R : Type u} [Ring R] [LinearOrder R] [IsOrdered R] {a b : R} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem Lean.Grind.Ring.IsOrdered.mul_pos_iff {R : Type u} [Ring R] [LinearOrder R] [IsOrdered R] {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem Lean.Grind.Ring.IsOrdered.sq_nonneg {R : Type u} [Ring R] [LinearOrder R] [IsOrdered R] {a : R} : 0 ≤ a ^ 2

theorem Lean.Grind.Ring.IsOrdered.sq_pos {R : Type u} [Ring R] [LinearOrder R] [IsOrdered R] {a : R} (h : a ≠ 0) : 0 < a ^ 2