{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
module Algebra.Apartness.Properties.HeytingCommutativeRing
{c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
open import Data.Product using (_,_; proj₂)
open import Algebra using (CommutativeRing; RightIdentity)
open HeytingCommutativeRing HCR
open CommutativeRing commutativeRing using (ring)
open import Algebra.Properties.Ring ring using (-0#≈0#)
x-0≈x : RightIdentity _≈_ 0# _-_
x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x)
1#0 : 1# # 0#
1#0 = invertible⇒# (1# , 1*[x-0]≈x , [x-0]*1≈x)
where
1*[x-0]≈x : ∀ {x} → 1# * (x - 0#) ≈ x
1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x)
[x-0]*1≈x : ∀ {x} → (x - 0#) * 1# ≈ x
[x-0]*1≈x {x} = trans (*-comm (x - 0#) 1#) 1*[x-0]≈x