diff --git a/CHANGELOG.md b/CHANGELOG.md
index e166023acc..b531a5d4a4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3284,6 +3284,24 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ↭-reverse : (xs : List A) → reverse xs ↭ xs
   ```
 
+* Added new functions to `Algebra.Properties.CommutativeMonoid`
+  ```agda
+  invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x
+  invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x
+  invertibleˡ⇒invertible  : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+  invertibleʳ⇒invertible  : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+  ```
+
+* Added new functions to `Algebra.Apartness.Bundles`
+  ```agda
+  invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+  invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+  x#0y#0→xy#0   : x # 0# → y # 0# → x * y # 0#
+  #-sym         : Symmetric _#_
+  #-congʳ       : x ≈ y → x # z → y # z
+  #-congˡ       : y ≈ z → x # y → x # z
+  ```
+
 * Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties`
   and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`.
   ```agda
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 1f04cc2dd0..7f4f164f42 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -11,23 +11,98 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Data.Product.Base using (_,_; proj₂)
-open import Algebra using (CommutativeRing; RightIdentity)
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
 
 open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring)
+open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
 
-open import Algebra.Properties.Ring ring using (-0#≈0#)
+open import Algebra.Properties.Ring ring
+  using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
+open import Relation.Binary.Definitions using (Symmetric)
+import Relation.Binary.Reasoning.Setoid as ReasonSetoid
+open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
 
+private variable
+  x y z : Carrier
+
+invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
+
+invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
 
 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)
+1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
   where
-  1*[x-0]≈x : ∀ {x} → 1# * (x - 0#) ≈ x
+  1*[x-0]≈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
+x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
+x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
+  where
+
+  helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0#
+  helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
+    = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
+    where
+    open ReasonSetoid setoid
+
+    y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
+    y⁻¹*x⁻¹*x*y≈1 = begin
+      y⁻¹ * x⁻¹ * (x * y - 0#)     ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
+      y⁻¹ * x⁻¹ * (x * y)          ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
+      y⁻¹ * (x⁻¹ * (x * y))       ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩
+      y⁻¹ * ((x⁻¹ * x) * y)       ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩
+      y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
+      y⁻¹ * (1# * y)               ≈⟨ *-congˡ (*-identityˡ y) ⟩
+      y⁻¹ * y                     ≈˘⟨ *-congˡ (x-0≈x y) ⟩
+      y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
+      1# ∎
+
+#-sym : Symmetric _#_
+#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
+  where
+  open ReasonSetoid setoid
+  InvX-Y : Invertible _≈_ 1# _*_ (x - y)
+  InvX-Y = #⇒invertible x#y
+
+  x-y⁻¹ = InvX-Y .proj₁
+
+  y-x≈-[x-y] : y - x ≈ - (x - y)
+  y-x≈-[x-y] = begin
+    y - x     ≈˘⟨ +-congʳ (-‿involutive y) ⟩
+    - - y - x ≈˘⟨ -‿anti-homo-+ x (- y) ⟩
+    - (x - y) ∎
+
+  x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
+  x-y⁻¹*y-x≈1 = begin
+    (- x-y⁻¹) * (y - x)   ≈˘⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟩
+    - (x-y⁻¹ * (y - x))    ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
+    - (x-y⁻¹ * - (x - y)) ≈˘⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟩
+    - - (x-y⁻¹ * (x - y))  ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
+    x-y⁻¹ * (x - y)        ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
+    1# ∎
+
+#-congʳ : x ≈ y → x # z → y # z
+#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z)
+  where
+
+  helper : Invertible _≈_ 1# _*_ (x - z) → y # z
+  helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
+    = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
+    where
+    open ReasonSetoid setoid
+
+    x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
+    x-z⁻¹*y-z≈1 = begin
+      x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩
+      x-z⁻¹ * (x - z)  ≈⟨ x-z⁻¹*x-z≈1# ⟩
+      1# ∎
+
+#-congˡ : y ≈ z → x # y → x # z
+#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y))
diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
index 091e88ec61..e83be61ac7 100644
--- a/src/Algebra/Properties/CommutativeMonoid.agda
+++ b/src/Algebra/Properties/CommutativeMonoid.agda
@@ -7,6 +7,8 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles
+open import Algebra.Definitions
+open import Data.Product using (_,_; proj₂)
 
 module Algebra.Properties.CommutativeMonoid
   {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where
@@ -23,3 +25,18 @@ open CommutativeMonoid M
   ; assoc     to +-assoc
   ; comm      to +-comm
   )
+
+private variable
+  x : Carrier
+
+invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x
+invertibleˡ⇒invertibleʳ {x} (-x , -x+x≈1) = -x , trans (+-comm x -x) -x+x≈1
+
+invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x
+invertibleʳ⇒invertibleˡ {x} (-x , x+-x≈1) = -x , trans (+-comm -x x) x+-x≈1
+
+invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+invertibleˡ⇒invertible left@(-x , -x+x≈1) = -x , -x+x≈1 , invertibleˡ⇒invertibleʳ left .proj₂
+
+invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x
+invertibleʳ⇒invertible right@(-x , x+-x≈1) = -x , invertibleʳ⇒invertibleˡ right .proj₂ , x+-x≈1