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

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

    open import Algebra using (Ring)

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

    open Ring R

    import Algebra.Properties.RingWithoutOne as RingWithoutOneProperties
    open import Function.Base using (_$_)
    open import Relation.Binary.Reasoning.Setoid setoid
    open import Algebra.Definitions _≈_

    ------------------------------------------------------------------------
    -- Export properties of rings without a 1#.

    open RingWithoutOneProperties ringWithoutOne public

    ------------------------------------------------------------------------
    -- Extra properties of 1#

    -1*x≈-x : ∀ x → - 1# * x ≈ - x
    -1*x≈-x x = begin
      - 1# * x    ≈⟨ -‿distribˡ-* 1# x ⟨
      - (1# * x)  ≈⟨ -‿cong ( *-identityˡ x ) ⟩
      - x         ∎