feat: lemmas about ordered rings and fields for grind

src/Init/Grind/CommRing/Field.lean

@@ -12,8 +12,8 @@ namespace Lean.Grind
 
 class Field (α : Type u) extends CommRing α, Inv α, Div α where
   div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
+  zero_ne_one : (0 : α) ≠ 1
   inv_zero : (0 : α)⁻¹ = 0
-  inv_one : (1 : α)⁻¹ = 1
   mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
 
 attribute [instance 100] Field.toInv Field.toDiv
@@ -25,6 +25,52 @@ variable [Field α] {a : α}
 theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 := by
   rw [CommSemiring.mul_comm, mul_inv_cancel h]
 
+theorem eq_inv_of_mul_eq_one (h : a * b = 1) : a = b⁻¹ := by
+  by_cases h' : b = 0
+  · subst h'
+    rw [Semiring.mul_zero] at h
+    exfalso
+    exact zero_ne_one h
+  · replace h := congrArg (fun x => x * b⁻¹) h
+    simpa [Semiring.mul_assoc, mul_inv_cancel h', Semiring.mul_one, Semiring.one_mul] using h
+
+theorem inv_one : (1 : α)⁻¹ = 1 :=
+  (eq_inv_of_mul_eq_one (Semiring.mul_one 1)).symm
+
+theorem inv_inv (a : α) : a⁻¹⁻¹ = a := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    exact mul_inv_cancel h
+
+theorem inv_neg (a : α) : (-a)⁻¹ = -a⁻¹ := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero, Ring.neg_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    simp [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg, Field.inv_mul_cancel h]
+
+theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
+  constructor
+  · intro w
+    by_cases h : a = 0
+    · subst h
+      rfl
+    · have := congrArg (fun x => x * a) w
+      dsimp at this
+      rw [Semiring.zero_mul, inv_mul_cancel h] at this
+      exfalso
+      exact zero_ne_one this.symm
+  · intro w
+    subst w
+    simp [Field.inv_zero]
+
+theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
+  rw [eq_comm, inv_eq_zero_iff, eq_comm]
+
 instance [IsCharP α 0] : NoNatZeroDivisors α where
   no_nat_zero_divisors := by
     intro a b h w

src/Init/Grind/Ordered.lean

@@ -6,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Grind.Ordered.PartialOrder
+import Init.Grind.Ordered.Order
 import Init.Grind.Ordered.Module
 import Init.Grind.Ordered.Ring
+import Init.Grind.Ordered.Field
 import Init.Grind.Ordered.Int

src/Init/Grind/Ordered/Field.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.CommRing.Field
+import Init.Grind.Ordered.Ring
+
+namespace Lean.Grind
+
+namespace Field.IsOrdered
+
+variable {R : Type u} [Field R] [LinearOrder R] [Ring.IsOrdered R]
+
+open Ring.IsOrdered
+
+theorem pos_of_inv_pos {a : R} (h : 0 < a⁻¹) : 0 < a := by
+  rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
+  · exact h'
+  · simpa [Field.inv_zero] using h
+  · exfalso
+    have := Ring.IsOrdered.mul_neg_of_pos_of_neg h h'
+    rw [inv_mul_cancel (Preorder.ne_of_lt h')] at this
+    exact Ring.IsOrdered.not_one_lt_zero this
+
+theorem inv_pos_iff {a : R} : 0 < a⁻¹ ↔ 0 < a := by
+  constructor
+  · exact pos_of_inv_pos
+  · intro h
+    rw [← Field.inv_inv a] at h
+    exact pos_of_inv_pos h
+
+theorem inv_neg_iff {a : R} : a⁻¹ < 0 ↔ a < 0 := by
+  have := inv_pos_iff (a := -a)
+  rw [Field.inv_neg] at this
+  simpa [IntModule.IsOrdered.neg_pos_iff]
+
+theorem inv_nonneg_iff {a : R} : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
+  simp [PartialOrder.le_iff_lt_or_eq, inv_pos_iff, Field.zero_eq_inv_iff]
+
+theorem inv_nonpos_iff {a : R} : a⁻¹ ≤ 0 ↔ a ≤ 0 := by
+  have := inv_nonneg_iff (a := -a)
+  rw [Field.inv_neg] at this
+  simpa [IntModule.IsOrdered.neg_nonneg_iff] using this
+
+private theorem mul_le_of_le_mul_inv {a b c : R} (h : 0 < c) (h' : a ≤ b * c⁻¹) : a * c ≤ b := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt h)
+
+private theorem le_mul_inv_of_mul_le {a b c : R} (h : 0 < b) (h' : a * b ≤ c) : a ≤ c * b⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+
+theorem le_mul_inv_iff_mul_le (a b : R) {c : R} (h : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b :=
+  ⟨mul_le_of_le_mul_inv h, le_mul_inv_of_mul_le h⟩
+
+private theorem mul_inv_le_iff_le_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := by
+  have := (le_mul_inv_iff_mul_le a c (inv_pos_iff.mpr h)).symm
+  simpa [Field.inv_inv] using this
+
+private theorem mul_lt_of_lt_mul_inv {a b c : R} (h : 0 < c) (h' : a < b * c⁻¹) : a * c < b := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_pos_right h' h
+
+private theorem lt_mul_inv_of_mul_lt {a b c : R} (h : 0 < b) (h' : a * b < c) : a < c * b⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+
+theorem lt_mul_inv_iff_mul_lt (a b : R) {c : R} (h : 0 < c) : a < b * c⁻¹ ↔ a * c < b :=
+  ⟨mul_lt_of_lt_mul_inv h, lt_mul_inv_of_mul_lt h⟩
+
+theorem mul_inv_lt_iff_lt_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := by
+  simpa [Field.inv_inv] using (lt_mul_inv_iff_mul_lt a c (inv_pos_iff.mpr h)).symm
+
+private theorem le_mul_of_le_mul_inv {a b c : R} (h : c < 0) (h' : a ≤ b * c⁻¹) : b ≤ a * c := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+
+private theorem mul_le_of_mul_inv_le {a b c : R} (h : b < 0) (h' : a * b⁻¹ ≤ c) : c * b ≤ a := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+
+private theorem mul_inv_le_of_mul_le {a b c : R} (h : b < 0) (h' : a * b ≤ c) : c * b⁻¹ ≤ a := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+
+private theorem le_mul_inv_of_le_mul {a b c : R} (h : c < 0) (h' : a ≤ b * c) : b ≤ a * c⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+
+theorem le_mul_inv_iff_le_mul_of_neg (a b : R) {c : R} (h : c < 0) : a ≤ b * c⁻¹ ↔ b ≤ a * c :=
+  ⟨le_mul_of_le_mul_inv h, le_mul_inv_of_le_mul h⟩
+
+theorem mul_inv_le_iff_mul_le_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ ≤ c ↔ c * b ≤ a :=
+  ⟨mul_le_of_mul_inv_le h, mul_inv_le_of_mul_le h⟩
+
+private theorem lt_mul_of_lt_mul_inv {a b c : R} (h : c < 0) (h' : a < b * c⁻¹) : b < a * c := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+
+private theorem mul_lt_of_mul_inv_lt {a b c : R} (h : b < 0) (h' : a * b⁻¹ < c) : c * b < a := by
+  simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+
+private theorem mul_inv_lt_of_mul_lt {a b c : R} (h : b < 0) (h' : a * b < c) : c * b⁻¹ < a := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+
+private theorem lt_mul_inv_of_lt_mul {a b c : R} (h : c < 0) (h' : a < b * c) : b < a * c⁻¹ := by
+  simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
+    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+
+theorem lt_mul_inv_iff_lt_mul_of_neg (a b : R) {c : R} (h : c < 0) : a < b * c⁻¹ ↔ b < a * c :=
+  ⟨lt_mul_of_lt_mul_inv h, lt_mul_inv_of_lt_mul h⟩
+
+theorem mul_inv_lt_iff_mul_lt_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ < c ↔ c * b < a :=
+  ⟨mul_lt_of_mul_inv_lt h, mul_inv_lt_of_mul_lt h⟩
+
+theorem mul_lt_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c < b * c ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_pos_right · h)
+
+theorem mul_lt_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a < c * b ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_left h' (inv_pos_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_pos_left · h)
+
+theorem mul_lt_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_neg_right · h)
+
+theorem mul_lt_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_left h' (inv_neg_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_neg_left · h)
+
+theorem mul_le_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c ≤ b * c ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonneg_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a ≤ c * b ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_left h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonneg_left · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonpos_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_left h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonpos_left · (Preorder.le_of_lt h))
+
+end Field.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Ordered/Module.lean

@@ -8,7 +8,7 @@ module
 prelude
 import Init.Data.Int.Order
 import Init.Grind.Module.Basic
-import Init.Grind.Ordered.PartialOrder
+import Init.Grind.Ordered.Order
 
 namespace Lean.Grind
 

src/Init/Grind/Ordered/Order.lean

@@ -34,9 +34,22 @@ theorem lt_of_le_of_lt {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := b
 theorem lt_trans {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c :=
   lt_of_lt_of_le h₁ (le_of_lt h₂)
 
-theorem lt_irrefl {a : α} (h : a < a) : False := by
+theorem lt_irrefl (a : α) : ¬ (a < a) := by
+  intro h
   simp [lt_iff_le_not_le] at h
 
+theorem ne_of_lt {a b : α} (h : a < b) : a ≠ b :=
+  fun w => lt_irrefl a (w.symm ▸ h)
+
+theorem ne_of_gt {a b : α} (h : a > b) : a ≠ b :=
+  fun w => lt_irrefl b (w.symm ▸ h)
+
+theorem not_ge_of_lt {a b : α} (h : a < b) : ¬b ≤ a :=
+  fun w => lt_irrefl a (lt_of_lt_of_le h w)
+
+theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b :=
+  fun w => lt_irrefl a (lt_trans h w)
+
 end Preorder
 
 class PartialOrder (α : Type u) extends Preorder α where
@@ -58,4 +71,26 @@ theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
 
 end PartialOrder
 
+class LinearOrder (α : Type u) extends PartialOrder α where
+  le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
+
+namespace LinearOrder
+
+variable {α : Type u} [LinearOrder α]
+
+theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
+  cases LinearOrder.le_total a b with
+  | inl h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => left; exact h
+    | inr h => right; left; exact h
+  | inr h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => right; right; exact h
+    | inr h => right; left; exact h.symm
+
+end LinearOrder
+
 end Lean.Grind

src/Init/Grind/Ordered/Ring.lean

@@ -13,7 +13,7 @@ namespace Lean.Grind
 
 class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrdered R where
   /-- In a strict ordered semiring, we have `0 < 1`. -/
-  zero_lt_one : 0 < 1
+  zero_lt_one : (0 : R) < 1
   /-- 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_left : ∀ {a b c : R}, a < b → 0 < c → c * a < c * b
@@ -23,7 +23,15 @@ class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrde
 
 namespace Ring.IsOrdered
 
-variable {R : Type u} [Ring R] [PartialOrder R] [Ring.IsOrdered R]
+variable {R : Type u} [Ring R]
+section PartialOrder
+
+variable [PartialOrder R] [Ring.IsOrdered R]
+
+theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one
+
+theorem not_one_lt_zero : ¬ ((1 : R) < 0) :=
+  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
 
 theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by
   rw [PartialOrder.le_iff_lt_or_eq] at h'
@@ -47,19 +55,104 @@ theorem mul_le_mul_of_nonneg_right {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a
     | inr h => subst h; exact Preorder.le_refl (a * c)
   | inr h' => subst h'; simp [Semiring.mul_zero, Preorder.le_refl]
 
+theorem mul_le_mul_of_nonpos_left {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : c * b ≤ c * a := by
+  have := mul_le_mul_of_nonneg_left h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+
+theorem mul_le_mul_of_nonpos_right {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : b * c ≤ a * c := by
+  have := mul_le_mul_of_nonneg_right h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+
+theorem mul_lt_mul_of_neg_left {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a := by
+  have := mul_lt_mul_of_pos_left h (IntModule.IsOrdered.neg_pos_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+
+theorem mul_lt_mul_of_neg_right {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c := by
+  have := mul_lt_mul_of_pos_right h (IntModule.IsOrdered.neg_pos_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+
 theorem mul_nonneg {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b := by
   simpa [Semiring.zero_mul] using mul_le_mul_of_nonneg_right h₁ h₂
 
+theorem mul_nonneg_of_nonpos_of_nonpos {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : 0 ≤ a * b := by
+  have := mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
+
+theorem mul_nonpos_of_nonneg_of_nonpos {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) : a * b ≤ 0 := by
+  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.mul_neg]
+  apply mul_nonneg h₁ (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+
+theorem mul_nonpos_of_nonpos_of_nonneg {a b : R} (h₁ : a ≤ 0) (h₂ : 0 ≤ b) : a * b ≤ 0 := by
+  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.neg_mul]
+  apply mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) h₂
+
 theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
   simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
 
-theorem sq_nonneg {a : R} (h : 0 ≤ a) : 0 ≤ a^2 := by
-  rw [Semiring.pow_two]
-  apply mul_nonneg h h
+theorem mul_pos_of_neg_of_neg {a b : R} (h₁ : a < 0) (h₂ : b < 0) : 0 < a * b := by
+  have := mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
 
-theorem sq_pos {a : R} (h : 0 < a) : 0 < a^2 := by
-  rw [Semiring.pow_two]
-  apply mul_pos h h
+theorem mul_neg_of_pos_of_neg {a b : R} (h₁ : 0 < a) (h₂ : b < 0) : a * b < 0 := by
+  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.mul_neg]
+  apply mul_pos h₁ (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+
+theorem mul_neg_of_neg_of_pos {a b : R} (h₁ : a < 0) (h₂ : 0 < b) : a * b < 0 := by
+  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.neg_mul]
+  apply mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) h₂
+
+end PartialOrder
+
+section LinearOrder
+
+variable [LinearOrder R] [Ring.IsOrdered R]
+
+theorem mul_nonneg_iff {a b : R} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
+  rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg]
+    · simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
+    · have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
+      simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
+        Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
+  · simp [Semiring.zero_mul, Preorder.le_refl, LinearOrder.le_total]
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
+      simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
+        Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
+    · simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
+    · simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg_of_nonpos_of_nonpos]
+
+theorem mul_pos_iff {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
+  rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · simp [ha, hb, mul_pos]
+    · simp [Preorder.lt_irrefl, Semiring.mul_zero]
+    · have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
+      simp [ha, hb, Preorder.not_gt_of_lt m,
+        Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
+  · simp [Preorder.lt_irrefl, Semiring.zero_mul]
+  · rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
+    · have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
+      simp [ha, hb, Preorder.not_gt_of_lt m,
+        Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
+    · simp [Preorder.lt_irrefl, Semiring.mul_zero]
+    · simp [ha, hb, mul_pos_of_neg_of_neg]
+
+theorem sq_nonneg {a : R} : 0 ≤ a^2 := by
+  rw [Semiring.pow_two, mul_nonneg_iff]
+  rcases LinearOrder.le_total 0 a with (h | h)
+  · exact .inl ⟨h, h⟩
+  · exact .inr ⟨h, h⟩
+
+theorem sq_pos {a : R} (h : a ≠ 0) : 0 < a^2 := by
+  rw [Semiring.pow_two, mul_pos_iff]
+  rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
+  · exact .inl ⟨h', h'⟩
+  · simp at h
+  · exact .inr ⟨h', h'⟩
+
+end LinearOrder
 
 end Ring.IsOrdered