    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some basic properties of RingWithoutOne
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra.Bundles using (RingWithoutOne)

    module Algebra.Properties.RingWithoutOne {r₁ r₂} (R : RingWithoutOne r₁ r₂) where

    open RingWithoutOne R

    import Algebra.Properties.AbelianGroup as AbelianGroupProperties
    open import Function.Base using (_$_)
    open import Relation.Binary.Reasoning.Setoid setoid

    ------------------------------------------------------------------------
    -- Export properties of abelian groups

    open AbelianGroupProperties +-abelianGroup public
      renaming
      ( ε⁻¹≈ε            to -0#≈0#
      ; ∙-cancelˡ        to +-cancelˡ
      ; ∙-cancelʳ        to +-cancelʳ
      ; ∙-cancel         to +-cancel
      ; ⁻¹-involutive    to -‿involutive
      ; ⁻¹-injective     to -‿injective
      ; ⁻¹-anti-homo-∙   to -‿anti-homo-+
      ; identityˡ-unique to +-identityˡ-unique
      ; identityʳ-unique to +-identityʳ-unique
      ; identity-unique  to +-identity-unique
      ; inverseˡ-unique  to +-inverseˡ-unique
      ; inverseʳ-unique  to +-inverseʳ-unique
      ; ⁻¹-∙-comm        to -‿+-comm
      )

    -‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
    -‿distribˡ-* x y = sym $ begin
      - x * y                        ≈⟨ +-identityʳ (- x * y) ⟨
      - x * y + 0#                   ≈⟨ +-congˡ $ -‿inverseʳ (x * y) ⟨
      - x * y + (x * y + - (x * y))  ≈⟨ +-assoc (- x * y) (x * y) (- (x * y)) ⟨
      - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ distribʳ y (- x) x ⟨
      (- x + x) * y + - (x * y)      ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ x ⟩
      0# * y + - (x * y)             ≈⟨ +-congʳ $ zeroˡ y ⟩
      0# + - (x * y)                 ≈⟨ +-identityˡ (- (x * y)) ⟩
      - (x * y)                      ∎

    -‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
    -‿distribʳ-* x y = sym $ begin
      x * - y                        ≈⟨ +-identityˡ (x * - y) ⟨
      0# + x * - y                   ≈⟨ +-congʳ $ -‿inverseˡ (x * y) ⟨
      - (x * y) + x * y + x * - y    ≈⟨ +-assoc (- (x * y)) (x * y) (x * - y) ⟩
      - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ distribˡ x y (- y) ⟨
      - (x * y) + x * (y + - y)      ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ y ⟩
      - (x * y) + x * 0#             ≈⟨ +-congˡ $ zeroʳ x ⟩
      - (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-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    ∎