Add +-*-commutativeSemiring bundle for Integer (#1293) (#1336)

Author: lexvanderstoep

CHANGELOG.md

@@ -112,3 +112,8 @@ Other minor additions
   take-drop-id : take m v ++ drop m v ≡ v
   zipWith-replicate : zipWith {n = n} _⊕_ (replicate x) (replicate y) ≡ replicate (x ⊕ y)
   ```
+
+* Add new properties to `Data.Integer.Properties`:
+  ```agda
+  +-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+  ```

src/Data/Integer/Properties.agda

@@ -1292,6 +1292,11 @@ private
   { isSemiring = +-*-isSemiring
   }
 
++-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
++-*-commutativeSemiring = record
+  { isCommutativeSemiring = +-*-isCommutativeSemiring
+  }
+
 +-*-ring : Ring 0ℓ 0ℓ
 +-*-ring = record
   { isRing = +-*-isRing