Add proofs for Ring and commutative semigroup

CHANGELOG.md

@@ -1617,6 +1617,7 @@ Other minor changes
   leftSemimedial : LeftSemimedial _∙_
   rightSemimedial : RightSemimedial _∙_
   middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
+  semimedial : Semimedial _∙_
   ```
 
 * Added new proofs to `Algebra.Properties.Semigroup`:
@@ -1630,6 +1631,9 @@ Other minor changes
 * Added new proofs to `Algebra.Properties.Ring`:
   ```agda
   -1*x≈-x : ∀ x → - 1# * x ≈ - x
+  x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
+  x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z
+  [y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x)
   ```
 
 * Added new definitions to `Algebra.Structures`:

src/Algebra/Properties/CommutativeSemigroup.agda

@@ -16,6 +16,7 @@ open CommutativeSemigroup CS
 
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
+open import Data.Product
 
 ------------------------------------------------------------------------------
 -- Re-export the contents of semigroup
@@ -168,3 +169,6 @@ middleSemimedial x y z = begin
   x ∙ ((z ∙ y) ∙ x) ≈⟨ ∙-congˡ ( assoc z y x) ⟩
   x ∙ (z ∙ (y ∙ x)) ≈⟨ sym (assoc x z ((y ∙ x))) ⟩
   (x ∙ z) ∙ (y ∙ x) ∎
+
+semimedial : Semimedial _∙_
+semimedial = semimedialˡ , semimedialʳ

src/Algebra/Properties/Ring.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Algebra
+open import Algebra using (Ring)
 
 module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where
 
@@ -15,6 +15,8 @@ open Ring R
 import Algebra.Properties.AbelianGroup as AbelianGroupProperties
 open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
+open import Algebra.Definitions _≈_
+open import Data.Product
 
 ------------------------------------------------------------------------
 -- Export properties of abelian groups
@@ -67,3 +69,17 @@ open AbelianGroupProperties +-abelianGroup public
   - (1# * x)  ≈⟨ -‿cong ( *-identityˡ x ) ⟩
   - x         ∎
 
+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-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    ∎
+
+[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    ∎