Provide binomial theorem for commutative semiring

CHANGELOG.md

@@ -133,6 +133,12 @@ New modules
   Function.Identity.Instances
   ```
 
+* Algerbaic properties:
+  ```agda
+  Algebra.Properties.CommutativeSemiring
+  Algebra.Properties.SemiringWithoutOne
+  ```
+
 * Predicate for lists that are sorted with respect to a total order
   ```
   Data.List.Relation.Unary.Sorted.TotalOrder
@@ -144,6 +150,12 @@ New modules
   Data.Nat.Binary.Subtraction
   ```
 
+* Combinatorics operations
+  ```
+  Data.Fin.Combinatorics
+  Data.Nat.Combinatorics
+  ```
+
 * A predicate for vectors in which every pair of elements is related.
   ```
   Data.Vec.Relation.Unary.AllPairs
@@ -240,6 +252,16 @@ Other minor additions
                       IsCommutativeRing _≈₁_ _+_ _*_ -_ 0# 1#
   ```
 
+* Added proofs to `Algebra.Properties.CommutativeMonoid`:
+  ```agda
+  sumₜ-init : sumₜ t ≈ sumₜ (init t) + lookup t (fromℕ n)
+  ```
+
+* Added declarations to `Algebra.Structures.IsSemiringWithoutOne`:
+  ```agda
+  distribˡ : * DistributesOverˡ +
+  ```
+
 * Added new proof to `Data.Fin.Induction`:
   ```agda
   <-wellFounded : WellFounded _<_
@@ -262,6 +284,14 @@ Other minor additions
   splitAt-<         : splitAt m {n} i ≡ inj₁ (fromℕ< i<m)
   splitAt-≥         : splitAt m {n} i ≡ inj₂ (reduce≥ i i≥m)
   inject≤-injective : inject≤ x n≤m ≡ inject≤ y n≤m′ → x ≡ y
+
+  k+nℕ-ℕk≡n            : toℕ k + (n ℕ-ℕ k) ≡ n
+  k≡fromℕ[n]⇒toℕ[k]≡n  : k ≡ fromℕ n → toℕ k ≡ n
+  toℕ[k]≡n⇒k≡fromℕ[n]  : toℕ k ≡ n → k ≡ fromℕ n
+  punchIn≡inject₁      : punchIn (fromℕ n) k ≡ inject₁ k
+  punchOut≡lower₁      : punchOut {i = fromℕ n} {j = i} n≢i′ ≡ lower₁ i n≢i
+  punchOut-irrelevant  : (p₁ p₂ : i ≢ j) → punchOut p₁ ≡ punchOut p₂
+
   ```
 
 * Added new functions to `Data.Fin.Base`:
@@ -379,6 +409,11 @@ Other minor additions
 
 * `Data.Nat.Binary.Induction` now re-exports `Acc` and `acc` from `Induction.WellFounded`.
 
+* Added new properties to `Data.Nat.Properties`:
+  ```agda
+  m≢0∧n≢0⇒m*n≢0 : m ≢ 0 → n ≢ 0 → m * n ≢ 0
+  ```
+
 * Added new properties to `Data.Nat.Binary.Properties`:
   ```agda
   +-isSemigroup            : IsSemigroup _+_
@@ -492,6 +527,13 @@ Other minor additions
   words   : String → List String
   ```
 
+* Added definitions to `Data.Table.Base`:
+  ```agda
+  last : ∀ {n} → Table A (suc n) → A
+  init : ∀ {n} → Table A (suc n) → Table A n
+  ```
+
+
 * Added new proofs to `Data.Tree.Binary.Properties`:
   ```agda
   map-compose : map (f₁ ∘ f₂) (g₁ ∘ g₂) ≗ map f₁ g₁ ∘ map f₂ g₂

src/Algebra/Properties/CommutativeMonoid.agda

@@ -19,10 +19,10 @@ open import Algebra.Solver.CommutativeMonoid M
 open import Relation.Binary as B using (_Preserves_⟶_)
 open import Function
 open import Function.Equality using (_⟨$⟩_)
-open import Data.Product
+open import Data.Product hiding (_×_)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Fin.Base using (Fin; zero; suc; fromℕ)
 open import Data.List.Base as List using ([]; _∷_)
 import Data.Fin.Properties as FP
 open import Data.Fin.Permutation as Perm using (Permutation; Permutation′; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
@@ -73,6 +73,20 @@ sumₜ-remove {suc n} {suc i}  t′ =
   ∑t = sumₜ t
   ∑t′ = sumₜ (remove i t)
 
+-- When summing over a function from a finite set, we can pull out last element
+
+sumₜ-init : ∀ {n} (t : Table Carrier (suc n)) → sumₜ t ≈ sumₜ (init t) + lookup t (fromℕ n)
+sumₜ-init {zero} t = +-comm (lookup t zero) 0#
+sumₜ-init {suc n} t = begin
+  t₀ + ∑t             ≈⟨ +-congˡ (sumₜ-init (tail t)) ⟩
+  t₀ + (∑t′ + tₗ)     ≈˘⟨ +-assoc _ _ _ ⟩
+  (t₀ + ∑t′) + tₗ     ∎
+  where
+    t₀ = head t
+    tₗ = last t
+    ∑t = sumₜ (tail t)
+    ∑t′ = sumₜ (tail (init t))
+
 -- '_≈_' is a congruence over 'sumTable n'.
 
 sumₜ-cong-≈ : ∀ {n} → sumₜ {n} Preserves _≋_ ⟶ _≈_

src/Algebra/Properties/CommutativeSemiring.agda

@@ -0,0 +1,157 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some basic properties of Rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- Disabled to prevent warnings from deprecated Table
+{-# OPTIONS --warn=noUserWarning #-}
+
+open import Algebra
+
+module Algebra.Properties.CommutativeSemiring {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where
+
+open CommutativeSemiring R
+open import Algebra.Properties.CommutativeMonoid +-commutativeMonoid
+open import Algebra.Properties.SemiringWithoutOne semiringWithoutOne
+open import Algebra.Operations.Semiring semiring
+
+import Data.Nat.Base as ℕ
+open import Data.Nat.Base using (ℕ; suc)
+import Data.Nat.Properties as ℕ
+open import Data.Nat.Properties using (≤-refl)
+import Data.Fin.Base as Fin
+open import Data.Fin.Base using (Fin; fromℕ; toℕ; punchIn; lower₁; inject₁; _ℕ-ℕ_)
+open import Data.Fin.Properties using (_≟_; toℕ[k]≡n⇒k≡fromℕ[n]; k≡fromℕ[n]⇒toℕ[k]≡n; toℕ-inject₁-≢; lower₁-inject₁′; suc-injective; lower₁-irrelevant; toℕ-lower₁)
+open import Data.Fin.Combinatorics using (_C_; nCn≡1)
+open import Data.Table.Base using (lookup; tabulate)
+
+open import Function using (_∘_)
+
+open import Relation.Binary.Reasoning.Setoid setoid
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+
+------------------------------------------------------------------------
+-- Properties of _^_
+
+binomial : ∀ n x y → ((x + y) ^ n) ≈ ∑[ i < suc n ] ((n C i) × (x ^ toℕ i) * (y ^ (n ℕ-ℕ i)))
+binomial ℕ.zero   x y = begin
+  ((x + y) ^ 0)                                             ≡⟨⟩
+  1#                                                        ≈˘⟨ *-identityʳ 1# ⟩
+  (1# * 1#)                                                 ≈˘⟨ *-congʳ (+-identityʳ 1#) ⟩
+  (1 × 1# * 1#)                                             ≡⟨⟩
+  (1 × (x ^ ℕ.zero) * (y ^ ℕ.zero))                         ≈˘⟨ +-identityʳ _ ⟩
+  ((0 C Fin.zero) × (x ^ ℕ.zero) * (y ^ ℕ.zero)) + 0#       ≡⟨⟩
+  (∑[ i < 1 ] ((0 C i) × (x ^ toℕ i) * (y ^ (0 ℕ-ℕ i))))    ∎
+binomial (suc n) x y = begin
+  ((x + y) ^ suc n)                                                       ≡⟨⟩
+  (x + y) * (x + y) ^ n                                                   ≈⟨ *-congˡ (binomial n x y) ⟩
+  (x + y) * ∑[ i < suc n ] bt n i                                         ≈⟨ distribʳ _ _ _ ⟩
+  x * ∑[ i < suc n ] bt n i + y * ∑[ i < suc n ] bt n i                   ≈⟨ +-cong lemma₃ lemma₄ ⟩
+  ∑[ i < suc (suc n) ] bt₁ n i + ∑[ i < suc (suc n) ] bt₂ n i             ≈˘⟨ ∑-distrib-+ _ (bt₁ n) (bt₂ n) ⟩
+  ∑[ i < suc (suc n) ] (bt₁ n i + bt₂ n i)                                ≈⟨ sumₜ-cong-≈ lemma₈ ⟩
+  ∑[ i < suc (suc n) ] bt (suc n) i ∎
+  where
+    bt : (n : ℕ) → (k : Fin (suc n)) → Carrier
+    bt n k = ((n C k) × (x ^ toℕ k) * (y ^ (n ℕ-ℕ k)))
+    bt₁ : (n : ℕ) → (k : Fin (suc (suc n))) → Carrier
+    bt₁ n Fin.zero = 0#
+    bt₁ n (Fin.suc k) = x * bt n k
+    bt₂ : (n : ℕ) → (k : Fin (suc (suc n))) → Carrier
+    bt₂ n k with k ≟ fromℕ (suc n)
+    ... | yes k≡1+n = 0#
+    ... | no  k≢1+n = y * bt n (lower₁ k (λ 1+n≡k → contradiction (toℕ[k]≡n⇒k≡fromℕ[n] (suc n) k (≡-sym 1+n≡k)) k≢1+n))
+    bbt : (n : ℕ) → (k : Fin (suc n)) → Carrier
+    bbt n k = (x ^ toℕ k) * (y ^ (n ℕ-ℕ k))
+    lemma₁ : ∀ k → y * bt n k ≈ bt₂ n (inject₁ k)
+    lemma₁ k with (inject₁ k) ≟ fromℕ (suc n)
+    ... | yes k≡1+n = contradiction (k≡fromℕ[n]⇒toℕ[k]≡n (suc n) (inject₁ k) k≡1+n) (toℕ-inject₁-≢ k ∘ ≡-sym)
+    ... | no  k≢1+n = sym (reflexive (cong (λ h → y * bt n h) (lower₁-inject₁′ k _)))
+    lemma₂ : 0# ≈ bt₂ n (fromℕ (suc n))
+    lemma₂ with fromℕ (suc n) ≟ fromℕ (suc n)
+    ... | yes 1+n≡1+n = refl
+    ... | no  1+n≢1+n = contradiction ≡-refl 1+n≢1+n
+    lemma₃ : x * ∑[ i < suc n ] bt n i ≈ ∑[ i < suc (suc n) ] bt₁ n i
+    lemma₃ = begin
+      (x * ∑[ i < suc n ] bt n i)                                   ≈⟨ *-distribˡ-∑ (suc n) (bt n) x ⟩
+      ∑[ i < suc n ] (x * bt n i)                                   ≈˘⟨ +-identityˡ _ ⟩
+      (0# + ∑[ i < suc n ] (x * bt n i))                            ≡⟨⟩
+      (0# + ∑[ i < suc n ] bt₁ n (punchIn Fin.zero i))              ≡⟨⟩
+      (∑[ i < suc (suc n) ] bt₁ n i)                                ∎
+    lemma₄ : y * ∑[ i < suc n ] bt n i ≈ ∑[ i < suc (suc n) ] bt₂ n i
+    lemma₄ = begin
+      (y * ∑[ i < suc n ] bt n i)                                                  ≈⟨ *-distribˡ-∑ (suc n) (bt n) y ⟩
+      ∑[ i < suc n ] (y * bt n i)                                                  ≈˘⟨ +-identityʳ _ ⟩
+      (∑[ i < suc n ] (y * bt n i) + 0#)                                           ≈⟨ +-cong (sumₜ-cong-≈ lemma₁) lemma₂ ⟩
+      ((∑[ i < suc n ] bt₂ n (inject₁ i)) + bt₂ n (fromℕ (suc n)))                 ≈˘⟨ sumₜ-init (tabulate (bt₂ n)) ⟩
+      sumₜ (tabulate (bt₂ n))                                                      ≡⟨⟩
+      ∑[ i < suc (suc n) ] bt₂ n i                                                 ∎
+    lemma₅ : ∀ k → x * bt n k ≈ (n C k) × bbt (suc n) (Fin.suc k)
+    lemma₅ k = begin
+      (x * bt n k)                                                                 ≡⟨⟩
+      (x * ((n C k) × x ^ toℕ k * y ^ (n ℕ-ℕ k)))                                  ≈˘⟨ *-assoc x ((n C k) × x ^ toℕ k) (y ^ (n ℕ-ℕ k)) ⟩
+      ((x * (n C k) × x ^ toℕ k) * y ^ (n ℕ-ℕ k))                                  ≈⟨ *-congʳ (×-comm (n C k) _ _) ⟩
+      (((n C k) × x ^ toℕ (Fin.suc k)) * y ^ (suc n ℕ-ℕ Fin.suc k))                ≈⟨ ×-assoc (n C k) _ _ ⟩
+      (n C k) × (x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k))                  ≡⟨⟩
+      (n C k) × bbt (suc n) (Fin.suc k)                                            ∎
+    lemma₆ : ∀ k 1+n≢1+k → y * bt n (lower₁ (Fin.suc k) 1+n≢1+k) ≈ (n C lower₁ (Fin.suc k) 1+n≢1+k) × bbt (suc n) (Fin.suc k)
+    lemma₆ k 1+n≢1+k = begin
+      (y * bt n 1+k)                                                               ≡⟨⟩
+      (y * ((n C 1+k) × x ^ toℕ 1+k * y ^ (n ℕ-ℕ 1+k)))                            ≈⟨ *-comm _ _ ⟩
+      (((n C 1+k) × x ^ toℕ 1+k * y ^ (n ℕ-ℕ 1+k)) * y)                            ≈⟨ *-assoc _ _ _ ⟩
+      ((n C 1+k) × x ^ toℕ 1+k * (y ^ (n ℕ-ℕ 1+k) * y))                            ≈⟨ *-congˡ (*-comm _ _) ⟩
+      ((n C 1+k) × x ^ toℕ 1+k * y ^ suc (n ℕ-ℕ 1+k))                              ≡⟨ cong (λ h → (n C 1+k) × x ^ h * y ^ suc (n ℕ-ℕ 1+k)) (toℕ-lower₁ (Fin.suc k) 1+n≢1+k) ⟩
+      ((n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ suc (n ℕ-ℕ 1+k))                      ≡⟨ cong (λ h → (n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ h) (1+[n-[1+k]]≡[1+n]-[1+k] n k 1+n≢1+k) ⟩
+      ((n C 1+k) × x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k))                ≈⟨ ×-assoc (n C 1+k) _ _ ⟩
+      ((n C 1+k) × (x ^ toℕ (Fin.suc k) * y ^ (suc n ℕ-ℕ Fin.suc k)))              ≡⟨⟩
+      ((n C 1+k) × bbt (suc n) (Fin.suc k))                                        ∎
+      where
+        1+k = lower₁ (Fin.suc k) 1+n≢1+k
+        1+[n-[1+k]]≡[1+n]-[1+k] : ∀ n k 1+n≢1+k → suc (n ℕ-ℕ lower₁ (Fin.suc k) 1+n≢1+k) ≡ suc n ℕ-ℕ Fin.suc k
+        1+[n-[1+k]]≡[1+n]-[1+k] ℕ.zero Fin.zero 1+n≢1+k = contradiction ≡-refl 1+n≢1+k
+        1+[n-[1+k]]≡[1+n]-[1+k] (suc n) Fin.zero 1+n≢1+k = ≡-refl
+        1+[n-[1+k]]≡[1+n]-[1+k] (suc n) (Fin.suc k) 1+n≢1+k = 1+[n-[1+k]]≡[1+n]-[1+k] n k (1+n≢1+k ∘ cong suc)
+    lemma₇ : ∀ k 1+n≢1+k → n C k ℕ.+ n C (lower₁ (Fin.suc k) 1+n≢1+k) ≡ (suc n C Fin.suc k)
+    lemma₇ k 1+n≢1+k with suc n ℕ.≟ toℕ (Fin.suc k)
+    ... | yes 1+n≡1+k = contradiction 1+n≡1+k 1+n≢1+k
+    ... | no  _       = cong (λ h → n C k ℕ.+ n C Fin.suc h) (lower₁-irrelevant k _ _)
+    lemma₈ : ∀ k → bt₁ n k + bt₂ n k ≈ bt (suc n) k
+    lemma₈ Fin.zero with Fin.zero ≟ fromℕ (suc n)
+    ... | yes ()
+    ... | no  0≢1+n = begin
+      bt₁ n Fin.zero + bt₂ n Fin.zero     ≡⟨⟩
+      0# + y * (1 × 1# * (y ^ n))         ≈⟨ +-identityˡ _ ⟩
+      y * (1 × 1# * (y ^ n))              ≈˘⟨ *-assoc _ _ _ ⟩
+      ((y * 1 × 1#) * y ^ n)              ≈⟨ *-congʳ (*-comm _ _) ⟩
+      ((1 × 1# * y) * y ^ n)              ≈⟨ *-assoc _ _ _ ⟩
+      (1 × 1# * (y * y ^ n))              ≡⟨⟩
+      (1 × 1# * (y ^ suc n))              ≡⟨⟩
+      bt (suc n) Fin.zero                 ∎
+    lemma₈ (Fin.suc k) with Fin.suc k ≟ fromℕ (suc n)
+    ... | yes 1+k≡1+n = begin
+      (x * bt n k) + 0#                                                                       ≈⟨ +-identityʳ _ ⟩
+      (x * bt n k)                                                                            ≡⟨ cong (λ h → x * bt n h) (suc-injective 1+k≡1+n) ⟩
+      (x * bt n (fromℕ n))                                                                    ≡⟨⟩
+      (x * ((n C fromℕ n) × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n))))                     ≡⟨ cong (λ h → x * (h × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n)))) (nCn≡1 n) ⟩
+      (x * (1 × (x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n))))                                 ≈⟨ *-congˡ (*-congʳ (+-identityʳ _)) ⟩
+      (x * ((x ^ toℕ (fromℕ n)) * (y ^ (n ℕ-ℕ fromℕ n))))                                     ≈˘⟨ *-assoc x _ _ ⟩
+      (x * (x ^ toℕ (fromℕ n))) * (y ^ (n ℕ-ℕ fromℕ n))                                       ≈˘⟨ *-congʳ (+-identityʳ _) ⟩
+      (1 × (x * (x ^ (toℕ (fromℕ n)))) * (y ^ (n ℕ-ℕ fromℕ n)))                               ≡˘⟨ cong (λ h → h × (x ^ toℕ (fromℕ (suc n))) * (y ^ (n ℕ-ℕ fromℕ n))) (nCn≡1 (suc n)) ⟩
+      ((suc n C fromℕ (suc n)) × (x ^ toℕ (fromℕ (suc n))) * (y ^ (suc n ℕ-ℕ fromℕ (suc n)))) ≡⟨⟩
+      bt (suc n) (fromℕ (suc n))                                                              ≡˘⟨ cong (λ h → bt (suc n) h) 1+k≡1+n ⟩
+      bt (suc n) (Fin.suc k)                                                                  ∎
+    ... | no  1+k≢1+n = begin
+      x * bt n k + y * bt n 1+k′                                                              ≈⟨ +-cong (lemma₅ k) (lemma₆ k laux) ⟩
+      (n C k) × bbt (suc n) (Fin.suc k) + (n C 1+k′) × bbt (suc n) (Fin.suc k)                ≈˘⟨ ×-homo-+ (bbt (suc n) (Fin.suc k)) (n C k) (n C 1+k′) ⟩
+      (n C k ℕ.+ n C 1+k′) × bbt (suc n) (Fin.suc k)                                          ≡⟨ cong (λ h → h × (bbt (suc n) (Fin.suc k))) (lemma₇ k laux) ⟩
+      (suc n C Fin.suc k) × bbt (suc n) (Fin.suc k)                                           ≈˘⟨ ×-assoc (suc n C Fin.suc k) (x ^ toℕ (Fin.suc k)) (y ^ (suc n ℕ-ℕ Fin.suc k)) ⟩
+      bt (suc n) (Fin.suc k)                                                                  ∎
+      where
+        laux : suc n ≢ toℕ (Fin.suc k)
+        laux 1+n≡1+k = contradiction (toℕ[k]≡n⇒k≡fromℕ[n] (suc n) (Fin.suc k) (≡-sym 1+n≡1+k)) 1+k≢1+n
+        1+k′ : Fin (suc n)
+        1+k′ = lower₁ (Fin.suc k) laux

src/Algebra/Properties/SemiringWithoutOne.agda

@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some derivable properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles
+
+module Algebra.Properties.SemiringWithoutOne
+  {g₁ g₂} (M : SemiringWithoutOne g₁ g₂) where
+
+open SemiringWithoutOne M
+open import Algebra.Definitions _≈_
+open import Algebra.Operations.CommutativeMonoid +-commutativeMonoid
+open import Data.Nat.Base using (ℕ; suc; zero)
+import Data.Fin.Base as Fin
+open import Data.Fin.Base using (Fin; suc)
+open import Data.Fin.Combinatorics using (_C_)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+*-distribˡ-∑ : ∀ n (f : Fin n → Carrier) x → x * (∑[ i < n ] f i) ≈ ∑[ i < n ] (x * (f i))
+*-distribˡ-∑ zero f x = zeroʳ x
+*-distribˡ-∑ (suc n) f x = begin
+  (x * (f₀ + ∑f))   ≈⟨ distribˡ _ _ _ ⟩
+  (x * f₀ + x * ∑f) ≈⟨ +-congˡ (*-distribˡ-∑ n _ _) ⟩
+  (x * f₀ + ∑xf)    ∎
+  where
+    f₀ = f Fin.zero
+    ∑f = ∑[ i < n ] f (suc i)
+    ∑xf = ∑[ i < n ] (x * f (suc i))
+
+*-distribʳ-∑ : ∀ n (f : Fin n → Carrier) x → (∑[ i < n ] f i) * x ≈ ∑[ i < n ] ((f i) * x)
+*-distribʳ-∑ zero f x = zeroˡ x
+*-distribʳ-∑ (suc n) f x = begin
+  ((f₀ + ∑f) * x)   ≈⟨ distribʳ _ _ _ ⟩
+  (f₀ * x + ∑f * x) ≈⟨ +-congˡ (*-distribʳ-∑ n _ _) ⟩
+  (f₀ * x + ∑fx)    ∎
+  where
+    f₀ = f Fin.zero
+    ∑f = ∑[ i < n ] f (suc i)
+    ∑fx = ∑[ i < n ] (f (suc i) * x)
+
+×-comm : ∀ n x y → x * (n × y) ≈ n × (x * y)
+×-comm zero x y = zeroʳ x
+×-comm (suc n) x y = begin
+  x * (suc n × y)       ≡⟨⟩
+  x * (y + n × y)       ≈⟨ distribˡ _ _ _ ⟩
+  x * y + x * (n × y)   ≈⟨ +-congˡ (×-comm n _ _) ⟩
+  x * y + n × (x * y)   ≡⟨⟩
+  suc n × (x * y)       ∎
+
+×-assoc : ∀ n x y → (n × x) * y ≈ n × (x * y)
+×-assoc zero x y = zeroˡ y
+×-assoc (suc n) x y = begin
+  (suc n × x) * y       ≡⟨⟩
+  (x + n × x) * y       ≈⟨ distribʳ _ _ _ ⟩
+  x * y + (n × x) * y   ≈⟨ +-congˡ (×-assoc n _ _) ⟩
+  x * y + n × (x * y)   ≡⟨⟩
+  suc n × (x * y)       ∎

src/Algebra/Structures.agda

@@ -313,6 +313,8 @@ record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
   open IsNearSemiring isNearSemiring public
     hiding (+-isMonoid; zeroˡ; *-isSemigroup)
 
+  distribˡ : * DistributesOverˡ +
+  distribˡ = proj₁ distrib
 
 record IsCommutativeSemiringWithoutOne
          (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where