From 43c73161f63d20b891a3ea74127eb86ed232f232 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Jul 2025 08:29:15 +0100
Subject: [PATCH] add: rule of signs for `RingWithoutOne`

---
 CHANGELOG.md                               | 10 +++++++---
 src/Algebra/Properties/RingWithoutOne.agda | 20 +++++++++++++++-----
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4b10f1a54e..1555c53894 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -254,9 +254,13 @@ Additions to existing modules
   ∣ˡ-preorder   : Preorder a ℓ _
   ```
 
-* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups
+* In `Algebra.Properties.RingWithoutOne`:
+  ```agda
+  [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
+  ```
 
-```
+* In `Algebra.Properties.Semigroup`, consequences for associativity for semigroups:
+  ```
   uv≈w⇒xu∙v≈xw          : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w
   uv≈w⇒u∙vx≈wx          : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x
   uv≈w⇒u[vx∙y]≈w∙xy     : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y)
@@ -275,7 +279,7 @@ Additions to existing modules
   uv≈wx⇒yu∙v≈yw∙x       : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x
   uv≈wx⇒u∙vy≈w∙xy       : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y)
   uv≈wx⇒yu∙vz≈yw∙xz     : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z)
-```
+  ```
 
 * In `Algebra.Properties.Semigroup.Divisibility`:
   ```agda
diff --git a/src/Algebra/Properties/RingWithoutOne.agda b/src/Algebra/Properties/RingWithoutOne.agda
index 5dda568cbc..d45edeaf0b 100644
--- a/src/Algebra/Properties/RingWithoutOne.agda
+++ b/src/Algebra/Properties/RingWithoutOne.agda
@@ -17,7 +17,7 @@ open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
--- Export properties of abelian groups
+-- Re-export abelian group properties for addition
 
 open AbelianGroupProperties +-abelianGroup public
   renaming
@@ -36,6 +36,12 @@ open AbelianGroupProperties +-abelianGroup public
   ; ⁻¹-∙-comm        to -‿+-comm
   )
 
+x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
+x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq
+
+------------------------------------------------------------------------
+-- Consequences of distributivity
+
 -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
 -‿distribˡ-* x y = sym $ begin
   - x * y                        ≈⟨ +-identityʳ (- x * y) ⟨
@@ -58,17 +64,21 @@ open AbelianGroupProperties +-abelianGroup public
   - (x * y) + 0#                 ≈⟨ +-identityʳ (- (x * y)) ⟩
   - (x * y)                      ∎
 
-x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
-x+x≈x⇒x≈0 x eq = +-identityˡ-unique x x eq
+[-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
+[-x][-y]≈xy x y = begin
+  - x * - y     ≈⟨ -‿distribˡ-* x (- y) ⟨
+  - (x * - y)   ≈⟨ -‿cong (-‿distribʳ-* x y) ⟨
+  - (- (x * y)) ≈⟨ -‿involutive (x * y) ⟩
+  x * y         ∎
 
 x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z
 x[y-z]≈xy-xz x y z = begin
   x * (y - z)      ≈⟨ distribˡ x y (- z) ⟩
-  x * y + x * - z  ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩
+  x * y + x * - z  ≈⟨ +-congˡ (-‿distribʳ-* x z) ⟨
   x * y - x * z    ∎
 
 [y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x)
 [y-z]x≈yx-zx x y z = begin
   (y - z) * x      ≈⟨ distribʳ x y (- z) ⟩
-  y * x + - z * x  ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩
+  y * x + - z * x  ≈⟨ +-congˡ (-‿distribˡ-* z x) ⟨
   y * x - z * x    ∎