diff --git a/CHANGELOG.md b/CHANGELOG.md
index d729b2b122..bcfb5671ab 100644
--- a/CHANGELOG.md
+++ b/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₂
diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
index 19dafdcdd0..5a1ce083ac 100644
--- a/src/Algebra/Properties/CommutativeMonoid.agda
+++ b/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 _≋_ ⟶ _≈_
diff --git a/src/Algebra/Properties/CommutativeSemiring.agda b/src/Algebra/Properties/CommutativeSemiring.agda
new file mode 100644
index 0000000000..ca525ff223
--- /dev/null
+++ b/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
diff --git a/src/Algebra/Properties/SemiringWithoutOne.agda b/src/Algebra/Properties/SemiringWithoutOne.agda
new file mode 100644
index 0000000000..3f25f2a275
--- /dev/null
+++ b/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)       ∎
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 4c2ce39da9..fd6343de69 100644
--- a/src/Algebra/Structures.agda
+++ b/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
diff --git a/src/Data/Fin/Combinatorics.agda b/src/Data/Fin/Combinatorics.agda
new file mode 100644
index 0000000000..24192b8854
--- /dev/null
+++ b/src/Data/Fin/Combinatorics.agda
@@ -0,0 +1,91 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Combinatorics operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Combinatorics where
+
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; lower₁; _ℕ-ℕ_)
+open import Data.Fin.Properties using (toℕ<n; toℕ-fromℕ; k+nℕ-ℕk≡n; toℕ-lower₁)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Combinatorics using (_!; n!≢0)
+open import Data.Nat.DivMod using (_/_)
+open import Data.Nat.Properties using (_≟_; 1+n≢0; m≢0∧n≢0⇒m*n≢0; *-identityʳ; *-identityˡ; suc-injective; *-distribˡ-+; *-distribʳ-+; *-assoc)
+open import Data.Nat.Solver
+
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (fromWitnessFalse)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; module ≡-Reasoning; inspect; [_])
+open import Function.Base using (_∘_)
+
+open ≡-Reasoning
+
+_C_ : (n : ℕ) → (k : Fin (suc n)) → ℕ
+n C zero = 1
+suc n C suc k with suc n ≟ toℕ (suc k)
+... | yes 1+n≡1+k = 1
+... | no  1+n≢1+k = (n C k) + (n C lower₁ (suc k) 1+n≢1+k)
+
+nCn≡1 : (n : ℕ) → n C fromℕ n ≡ 1
+nCn≡1 zero = refl
+nCn≡1 (suc n) with suc n ≟ toℕ (fromℕ (suc n))
+... | yes 1+n≡1+k = refl
+... | no  1+n≢1+k = contradiction (cong suc (sym (toℕ-fromℕ n))) 1+n≢1+k
+
+k!*[n-k]!*nCk≡n! : ∀ n k → toℕ k ! * (n ℕ-ℕ k) ! * n C k ≡ n !
+k!*[n-k]!*nCk≡n!  zero    zero   = refl
+k!*[n-k]!*nCk≡n! (suc n)  zero   = begin
+  1 * (suc n !) * 1                    ≡⟨ *-identityʳ (1 * suc n !) ⟩
+  1 * (suc n !)                        ≡⟨ *-identityˡ (suc n !) ⟩
+  (suc n !)                            ∎
+k!*[n-k]!*nCk≡n! (suc n) (suc k) with suc n ≟ toℕ (suc k)
+... | yes 1+n≡1+k = begin
+  (toℕ (suc k) !) * ((suc n ℕ-ℕ suc k) !) * 1 ≡˘⟨ cong (λ h → (h !) * (((suc n ℕ-ℕ suc k) !)) * 1) 1+n≡1+k ⟩
+  suc n ! * ((suc n ℕ-ℕ suc k) !) * 1         ≡⟨ *-identityʳ _ ⟩
+  suc n ! * ((suc n ℕ-ℕ suc k) !)             ≡⟨ cong (λ h → suc n ! * h !) (n-n≡0 (suc n) (suc k) 1+n≡1+k) ⟩
+  suc n ! * 0 !                               ≡⟨⟩
+  suc n ! * 1                                 ≡⟨ *-identityʳ _ ⟩
+  suc n !                                     ∎
+  where
+    n-n≡0 : ∀ n k → (n ≡ toℕ k) → n ℕ-ℕ k ≡ 0
+    n-n≡0  zero    zero   n≡k = refl
+    n-n≡0 (suc n) (suc k) n≡k = n-n≡0 n k (suc-injective n≡k)
+... | no  1+n≢1+k = begin
+  (toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !) * (n C k + n C k+1)                                         ≡⟨ *-distribˡ-+ ((toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !)) (n C k) (n C k+1) ⟩
+  (toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !) * n C k + (toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !) * n C k+1 ≡⟨ cong (λ h → h + ((toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !) * n C k+1)) lemma₃ ⟩
+  toℕ (suc k) * n ! + (toℕ (suc k)) ! * ((suc n ℕ-ℕ suc k) !) * n C k+1                               ≡⟨ cong (λ h → toℕ (suc k) * n ! + h) lemma₅ ⟩
+  toℕ (suc k) * n ! + (suc n ℕ-ℕ suc k) * n !                                                         ≡˘⟨ *-distribʳ-+ (n !) (toℕ (suc k)) _ ⟩
+  (toℕ (suc k) + (suc n ℕ-ℕ suc k)) * n !                                                             ≡⟨ cong (_* n !) (k+nℕ-ℕk≡n (suc n) (suc k)) ⟩
+  (suc n) * n !                                                                                       ≡⟨⟩
+  (suc n) !                                                                                           ∎
+  where
+    open +-*-Solver
+    k+1 = lower₁ (suc k) 1+n≢1+k
+    lemma₁ : ∀ a b c d → a * b * c * d ≡ a * (b * c * d)
+    lemma₁ = solve 4 (λ a b c d → ((a :* b) :* c) :* d := a :* ((b :* c) :* d)) refl
+    lemma₂ : ∀ a b c d → a * (b * c) * d ≡ b * (a * c * d)
+    lemma₂ = solve 4 (λ a b c d → (a :* (b :* c)) :* d := b :* ((a :* c) :* d)) refl
+    lemma₃ : toℕ (suc k) ! * (n ℕ-ℕ k) ! * n C k ≡ toℕ (suc k) * n !
+    lemma₃ = begin
+      toℕ (suc k) ! * (n ℕ-ℕ k) ! * n C k                                                             ≡⟨⟩
+      ((toℕ (suc k) * toℕ k !) * (n ℕ-ℕ k) !) * n C k                                                 ≡⟨ lemma₁ (toℕ (suc k)) (toℕ k !) ((n ℕ-ℕ k) !) (n C k) ⟩
+      toℕ (suc k) * (toℕ k ! * (n ℕ-ℕ k) ! * n C k)                                                   ≡⟨ cong (toℕ (suc k) *_) (k!*[n-k]!*nCk≡n! n k) ⟩
+      toℕ (suc k) * n !                                                                               ∎
+    lemma₄ : ∀ n k 1+n≢1+k → suc n ℕ-ℕ suc k ≡ suc (n ℕ-ℕ lower₁ (suc k) 1+n≢1+k)
+    lemma₄  zero    zero   1+n≢1+k = contradiction refl 1+n≢1+k
+    lemma₄ (suc n)  zero   1+n≢1+k = refl
+    lemma₄ (suc n) (suc k) 1+n≢1+k = lemma₄ n k (1+n≢1+k ∘ cong suc)
+    lemma₅ : toℕ (suc k) ! * (n ℕ-ℕ k) ! * n C k+1 ≡ (suc n ℕ-ℕ suc k) * n !
+    lemma₅ = begin
+      toℕ (suc k) ! *  (    n ℕ-ℕ     k) !                * n C k+1                                   ≡⟨⟩
+      toℕ (suc k) ! *  (suc n ℕ-ℕ suc k) !                * n C k+1                                   ≡⟨ cong (λ h → toℕ (suc k) ! * h ! * n C k+1) (lemma₄ n k 1+n≢1+k) ⟩
+      toℕ (suc k) ! *  suc (n ℕ-ℕ k+1)   !                * n C k+1                                   ≡⟨⟩
+      toℕ (suc k) ! * (suc (n ℕ-ℕ k+1)   * (n ℕ-ℕ k+1) !) * n C k+1                                   ≡˘⟨ cong (λ h → h ! * (suc (n ℕ-ℕ k+1)   * (n ℕ-ℕ k+1) !) * n C k+1) (toℕ-lower₁ (suc k) 1+n≢1+k) ⟩
+      toℕ    k+1  ! * (suc (n ℕ-ℕ k+1)   * (n ℕ-ℕ k+1) !) * n C k+1                                   ≡⟨ lemma₂ (toℕ k+1 !) (suc (n ℕ-ℕ k+1)) ((n ℕ-ℕ k+1) !) (n C k+1) ⟩
+      suc (n ℕ-ℕ k+1)   * (toℕ k+1 !     * (n ℕ-ℕ k+1) !  * n C k+1)                                  ≡⟨ cong (suc (n ℕ-ℕ k+1) *_) (k!*[n-k]!*nCk≡n! n k+1) ⟩
+      suc (n ℕ-ℕ k+1)   * n !                                                                         ≡˘⟨ cong (_* n !) (lemma₄ n k 1+n≢1+k) ⟩
+      (suc n ℕ-ℕ suc k) * n !                                                                         ∎
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index c10e92e8cd..5036090146 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -134,6 +134,14 @@ fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 ≤fromℕ : ∀ {n} → (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
 ≤fromℕ {n} i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ n)) (ℕₚ.≤-pred (toℕ<n i))
 
+k≡fromℕ[n]⇒toℕ[k]≡n : ∀ n k → .(k ≡ fromℕ n) → toℕ k ≡ n
+k≡fromℕ[n]⇒toℕ[k]≡n  zero    0F     k≡fromℕ[n] = refl
+k≡fromℕ[n]⇒toℕ[k]≡n (suc n) (suc k) k≡fromℕ[n] = cong suc (k≡fromℕ[n]⇒toℕ[k]≡n n k (suc-injective k≡fromℕ[n]))
+
+toℕ[k]≡n⇒k≡fromℕ[n] : ∀ n k → .(toℕ k ≡ n) → k ≡ fromℕ n
+toℕ[k]≡n⇒k≡fromℕ[n] zero 0F toℕ[k]≡n = refl
+toℕ[k]≡n⇒k≡fromℕ[n] (suc n) (suc k) toℕ[k]≡n = cong suc (toℕ[k]≡n⇒k≡fromℕ[n] n k (ℕₚ.suc-injective toℕ[k]≡n))
+
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
@@ -567,6 +575,10 @@ nℕ-ℕi≤n (suc n) (suc i)  = begin
   suc n    ∎
   where open ℕₚ.≤-Reasoning
 
+k+nℕ-ℕk≡n : ∀ n k → toℕ k ℕ.+ (n ℕ-ℕ k) ≡ n
+k+nℕ-ℕk≡n n 0F = ℕₚ.+-identityˡ n
+k+nℕ-ℕk≡n (suc n) (suc k) = cong suc (k+nℕ-ℕk≡n n k)
+
 ------------------------------------------------------------------------
 -- punchIn
 ------------------------------------------------------------------------
@@ -581,6 +593,10 @@ punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 =
 punchInᵢ≢i : ∀ {m} i (j : Fin m) → punchIn i j ≢ i
 punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
 
+punchIn≡inject₁ : ∀ {n} (k : Fin n) → punchIn (fromℕ n) k ≡ inject₁ k
+punchIn≡inject₁ {suc n}  0F     = refl
+punchIn≡inject₁ {suc n} (suc k) = cong suc (punchIn≡inject₁ k)
+
 ------------------------------------------------------------------------
 -- punchOut
 ------------------------------------------------------------------------
@@ -629,6 +645,17 @@ punchOut-punchIn (suc i) {suc j} = cong suc (begin
   j                                                           ∎)
   where open ≡-Reasoning
 
+punchOut-irrelevant : ∀ {n} {i j : Fin (suc n)} → (p₁ p₂ : i ≢ j) → punchOut p₁ ≡ punchOut p₂
+punchOut-irrelevant {_}     {0F}    {0F}    p₁ p₂ = contradiction refl p₁
+punchOut-irrelevant {_}     {0F}    {suc j} p₁ p₂ = refl
+punchOut-irrelevant {suc n} {suc i} {0F}    p₁ p₂ = refl
+punchOut-irrelevant {suc n} {suc i} {suc j} p₁ p₂ = cong suc (punchOut-irrelevant (p₁ ∘ cong suc) (p₂ ∘ cong suc))
+
+punchOut≡lower₁ : ∀ {n} {i : Fin (suc n)} → (n≢i : n ≢ toℕ i) → (n≢i′ : fromℕ n ≢ i) → punchOut {i = fromℕ n} {j = i} n≢i′ ≡ lower₁ i n≢i
+punchOut≡lower₁ {zero}  {0F}    n≢i _    = contradiction refl n≢i
+punchOut≡lower₁ {suc n} {0F}    n≢i _    = refl
+punchOut≡lower₁ {suc n} {suc i} n≢i n≢i′ = cong suc (punchOut≡lower₁ _ _)
+
 ------------------------------------------------------------------------
 -- Quantification
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda
new file mode 100644
index 0000000000..dcd0e5a48f
--- /dev/null
+++ b/src/Data/Nat/Combinatorics.agda
@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Combinatorics operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Combinatorics where
+open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s; _+_; _*_)
+open import Data.Nat.Properties using (*-mono-≤; module ≤-Reasoning; m≢0∧n≢0⇒m*n≢0; 1+n≢0)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+open import Relation.Nullary.Negation using (contradiction)
+
+_! : ℕ → ℕ
+zero ! = 1
+suc n ! = (suc n) * n !
+
+1≤n! : ∀ n → 1 ≤ n !
+1≤n! zero = s≤s z≤n
+1≤n! (suc n) = begin
+  1                     ≡⟨⟩
+  1 * 1                 ≤⟨ *-mono-≤ (s≤s (z≤n {n = n})) (1≤n! n) ⟩
+  suc n * n !           ≡⟨⟩
+  (suc n !)             ∎
+  where
+    open ≤-Reasoning
+
+n!≢0 : ∀ n → n ! ≢ 0
+n!≢0 zero ()
+n!≢0 (suc n) n!≡0 = m≢0∧n≢0⇒m*n≢0 (1+n≢0 {n}) (n!≢0 n) n!≡0
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index afbbbfc7bb..e787b0ddef 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -839,6 +839,11 @@ m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
 m*n≡0⇒m≡0∨n≡0 zero    {n}     eq = inj₁ refl
 m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  eq = inj₂ refl
 
+m≢0∧n≢0⇒m*n≢0 : ∀ {m n} → m ≢ 0 → n ≢ 0 → m * n ≢ 0
+m≢0∧n≢0⇒m*n≢0 {zero}  {n}     m≢0 n≢0 = contradiction refl m≢0
+m≢0∧n≢0⇒m*n≢0 {suc m} {zero}  m≢0 n≢0 = contradiction refl n≢0
+m≢0∧n≢0⇒m*n≢0 {suc m} {suc n} m≢0 n≢0 = 1+n≢0
+
 m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1
 m*n≡1⇒m≡1 (suc zero)    n             _  = refl
 m*n≡1⇒m≡1 (suc (suc m)) (suc zero)    ()
diff --git a/src/Data/Table/Base.agda b/src/Data/Table/Base.agda
index a7b282bd38..5b02d613bd 100644
--- a/src/Data/Table/Base.agda
+++ b/src/Data/Table/Base.agda
@@ -50,6 +50,12 @@ uncons t = head t , tail t
 remove : ∀ {n} → Fin (suc n) → Table A (suc n) → Table A n
 remove i t = tabulate (lookup t ∘ punchIn i)
 
+last : ∀ {n} → Table A (suc n) → A
+last {n = n} t = lookup t (fromℕ n)
+
+init : ∀ {n} → Table A (suc n) → Table A n
+init t = tabulate (lookup t ∘ inject₁)
+
 ------------------------------------------------------------------------
 -- Operations for transforming tables