opposite of a Ring [clean version of pr #1900]

CHANGELOG.md

@@ -1620,6 +1620,41 @@ 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
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _