class Lean.Grind.OrderedRing (R : Type u) [Semiring R] [Preorder R] extends Lean.Grind.OrderedAdd R : Prop

A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation, and multiplication are compatible with the preorder, and 0 < 1.

• add_le_left_iff {a b : R} (c : R) : a ≤ b ↔ a + c ≤ b + c
• 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.OrderedRing.neg_one_lt_zero {R : Type u} [Ring R] [Preorder R] [OrderedRing R] : -1 < 0

theorem Lean.Grind.OrderedRing.ofNat_nonneg {R : Type u} [Ring R] [Preorder R] [OrderedRing R] (x : Nat) : OfNat.ofNat x ≥ 0

instance Lean.Grind.OrderedRing.instIsCharPOfNatNat {α : Type u_1} [Ring α] [Preorder α] [OrderedRing α] : IsCharP α 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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