Revert "opposite of a Ring [clean version of pr #1900] (#1910)"

This reverts commit 7772dee.

Author: jamesmckinna

CHANGELOG.md

@@ -1664,41 +1664,6 @@ Other minor changes
   moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
-* Added new functions and proofs to `Algebra.Construct.Flip.Op`:
-  ```agda
-  zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
-  distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
-  isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# →
-                                      IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1#
-  isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1#
-  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# →
-                          IsCommutativeSemiring + (flip *) 0# 1#
-  isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# →
-                                      IsCancellativeCommutativeSemiring + (flip *) 0# 1#
-  isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# →
-                         IsIdempotentSemiring + (flip *) 0# 1#
-  isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1#
-  isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0#
-  isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# →
-                         IsNonAssociativeRing + (flip *) - 0# 1#
-  isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
-  isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# -
-  isCommutativeRing : IsCommutativeRing + * - 0# 1# →
-                      IsCommutativeRing + (flip *) - 0# 1#
-  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ →
-                                    SemiringWithoutAnnihilatingZero a ℓ
-  commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ
-  cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ →
-                                  CancellativeCommutativeSemiring a ℓ
-  idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ
-  quasiring : Quasiring a ℓ → Quasiring a ℓ
-  ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ
-  nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ
-  nearring : Nearring a ℓ → Nearring a ℓ
-  ring : Ring a ℓ → Ring a ℓ
-  commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ
-  ```
-
 * Added new definition to `Algebra.Definitions`:
   ```agda
   SelfInverse : Op₁ A → Set _