refactor: another attempt to resolve merge of agda#2576

Author: jamesmckinna

Diff for: CHANGELOG.md

@@ -42,6 +42,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Apartness.Properties.HeytingCommutativeRing`:
+  ```agda
+  x-0≈x  ↦   Algebra.Properties.Ring.x-0#≈x
+  #-sym  ↦   Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym
+  ```
+
 * In `Algebra.Definitions.RawMagma`:
   ```agda
   _∣∣_   ↦  _∥_

Diff for: src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -13,7 +13,7 @@ module Algebra.Apartness.Properties.HeytingCommutativeRing
 
 open import Algebra.Bundles using (CommutativeRing)
 
-open HeytingCommutativeRing HCR
+open HeytingCommutativeRing HCR using (commutativeRing)
 open CommutativeRing commutativeRing using (ring)
 open import Algebra.Properties.Ring ring using (x-0#≈x)
 
@@ -31,3 +31,9 @@ x-0≈x = x-0#≈x
 "Warning: x-0≈x was deprecated in v2.3.
 Please use Algebra.Properties.Ring.x-0#≈x instead."
 #-}
+
+open HeytingCommutativeRing HCR public using (#-sym)
+{-# WARNING_ON_USAGE #-sym
+"Warning: #-sym was deprecated in v2.3.
+Please use Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym instead."
+#-}

Diff for: src/Algebra/Apartness/Properties/HeytingField.agda

@@ -66,30 +66,6 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
       y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
       1#                           ∎
 
-#-sym : Symmetric _#_
-#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
-  where
-  open ≈-Reasoning 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 = helper ∘ #⇒invertible
   where