Add a consequence of definition straight to IsCancellativeCommutativeSemiring

CHANGELOG.md

@@ -249,6 +249,12 @@ Additions to existing modules
   x \\ y = (x ⁻¹) ∙ y
   ```
 
+* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the
+  extra property as an exposed definition:
+  ```agda
+    *-cancelʳ-nonZero : AlmostRightCancellative 0# *
+  ```
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)

src/Algebra/Structures.agda

@@ -573,6 +573,10 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a 
 
   open IsCommutativeSemiring isCommutativeSemiring public
 
+  *-cancelʳ-nonZero : AlmostRightCancellative 0# *
+  *-cancelʳ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ setoid
+      *-comm *-cancelˡ-nonZero
+
 record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   field
     isSemiring     : IsSemiring + * 0# 1#