From 3c0de494b5b38cb8e205d00e0f605679f577c896 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 14 Feb 2023 15:21:13 +0000
Subject: [PATCH 01/19] proofs of the Binomial Theorem

---
 CHANGELOG.md                                  |   6 +
 .../CommutativeSemiring/Binomial.agda         |  28 ++
 src/Algebra/Properties/Semiring/Binomial.agda | 282 ++++++++++++++++++
 3 files changed, 316 insertions(+)
 create mode 100644 src/Algebra/Properties/CommutativeSemiring/Binomial.agda
 create mode 100644 src/Algebra/Properties/Semiring/Binomial.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 93b707d2ba..17ef715fc7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1577,6 +1577,12 @@ New modules
   Algebra.Properties.Loop
   ```
 
+* Properties of (Commutative)Semiring: the Binomial Theorem
+  ```
+  Algebra.Properties.CommutativeSemiring.Binomial
+  Algebra.Properties.Semiring.Binomial
+  ```
+
 * Some n-ary functions manipulating lists
   ```
   Data.List.Nary.NonDependent
diff --git a/src/Algebra/Properties/CommutativeSemiring/Binomial.agda b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
new file mode 100644
index 0000000000..6527e6f862
--- /dev/null
+++ b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Binomial Theorem for Commutative Semirings
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles
+  using (CommutativeSemiring)
+
+module Algebra.Properties.CommutativeSemiring.Binomial {a ℓ} (S : CommutativeSemiring a ℓ) where
+
+open CommutativeSemiring S
+open import Algebra.Properties.Semiring.Exp semiring using (_^_)
+import Algebra.Properties.Semiring.Binomial semiring as Binomial
+open Binomial public hiding (theorem)
+
+------------------------------------------------------------------------
+-- Here it is
+
+theorem : ∀ n x y → ((x + y) ^ n) ≈ Binomial.expansion x y n
+theorem n x y = Binomial.theorem x y (*-comm x y) n
+
+
+
+
+
diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
new file mode 100644
index 0000000000..671b209bf2
--- /dev/null
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -0,0 +1,282 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Binomial Theorem for *-commuting elements in a Semiring
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (Semiring)
+open import Data.Nat.Base as Nat hiding (_+_; _*_; _^_)
+open import Data.Nat.Combinatorics
+  using (_C_; nCn≡1; nC1≡n; nCk+nC[k+1]≡[n+1]C[k+1])
+open import Data.Nat.Properties as Nat
+  using (n<ᵇ1+n; n∸n≡0; [m-n-1]+1≡[m-n])
+open import Data.Fin.Base as Fin
+  using (Fin; zero; suc; toℕ; fromℕ; inject₁)
+open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Properties as Fin
+  using (toℕ<n; toℕ-inject₁)
+open import Data.Fin.Relation.Unary.TopView
+  using (view; top; inj; view-inj; view-top; view-top-toℕ; module Instances)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; cong; module ≡-Reasoning)
+
+module Algebra.Properties.Semiring.Binomial {a ℓ} (S : Semiring a ℓ) where
+
+open Semiring S
+open import Algebra.Definitions _≈_
+open import Algebra.Structures _≈_
+open import Algebra.Properties.Semiring.Sum S
+open import Algebra.Properties.Semiring.Mult S
+open import Algebra.Properties.Semiring.Exp S
+import Relation.Binary.Reasoning.Setoid setoid as ≈-Reasoning
+
+
+------------------------------------------------------------------------
+-- The Binomial Theorem for *-commuting elements in a Semiring
+-- Freely adapted from PR #1287 by Maciej Piechotka (@uzytkownik)
+
+module _ (x y : Carrier) where
+
+------------------------------------------------------------------------
+-- Definitions
+
+  module Binomial (n : ℕ) where
+
+    module _ (i : Fin (suc n)) where
+
+      private
+        k   = toℕ i
+        n-k = n ∸ k
+
+      binomial : Carrier
+      binomial = (x ^ k) * (y ^ n-k)
+
+      term : Carrier
+      term = (n C k) × binomial
+
+    expansion : Carrier
+    expansion = ∑[ i < suc n ] term i
+
+    term₁ : (i : Fin (suc (suc n))) → Carrier
+    term₁ zero    = 0#
+    term₁ (suc i) = x * term i
+
+    sum₁ : Carrier
+    sum₁ = ∑[ i < suc (suc n) ] term₁ i
+
+    term₂ : (i : Fin (suc (suc n))) → Carrier
+    term₂ i with view i
+    ... | top   = 0#
+    ... | inj j = y * term j
+
+    sum₂ : Carrier
+    sum₂ = ∑[ i < suc (suc n) ] term₂ i
+
+------------------------------------------------------------------------
+-- Properties
+
+  module BinomialLemmas (n : ℕ) where
+
+    open Binomial n
+
+    open ≈-Reasoning
+
+    lemma₁ : x * expansion ≈ sum₁
+    lemma₁ = begin
+      x * expansion
+        ≈⟨ *-distribˡ-sum x term ⟩
+      ∑[ i < suc n ] (x * term i)
+        ≈˘⟨ +-identityˡ _ ⟩
+      (0# + ∑[ i < suc n ] (x * term i))
+        ≡⟨⟩
+      (0# + ∑[ i < suc n ] term₁ (suc i))
+        ≡⟨⟩
+      sum₁  ∎
+
+    lemma₂ : y * expansion ≈ sum₂
+    lemma₂ = begin
+      (y * expansion)
+        ≈⟨ *-distribˡ-sum y term ⟩
+      ∑[ i < suc n ] (y * term i)
+        ≈˘⟨ +-identityʳ _ ⟩
+      ∑[ i < suc n ] (y * term i) + 0#
+        ≈⟨ +-cong (sum-cong-≋ lemma₂-inj) lemma₂-top ⟩
+      (∑[ i < suc n ] term₂-inj i) + term₂ [n+1]
+        ≈˘⟨ sum-init term₂ ⟩
+      sum term₂
+        ≡⟨⟩
+      sum₂  ∎
+      where
+        [n+1] = fromℕ (suc n)
+
+        lemma₂-top : 0# ≈ term₂ [n+1]
+        lemma₂-top rewrite view-top (suc n) = refl
+
+        term₂-inj : (i : Fin (suc n)) → Carrier
+        term₂-inj i = term₂ (inject₁ i)
+
+        lemma₂-inj : ∀ i → y * term i ≈ term₂-inj i
+        lemma₂-inj i rewrite view-inj i = refl
+
+------------------------------------------------------------------------
+-- Next, a lemma which is independent of commutativity
+
+  module _ {n} (i : Fin (suc n)) where
+
+    open Binomial n using (term)
+
+    x*lemma : x * term i ≈ (n C toℕ i) × Binomial.binomial (suc n) (suc i)
+    x*lemma = begin
+      x * term i                                  ≡⟨⟩
+      x * ((n C k) × (x ^ k * y ^ (n ∸ k)))       ≈˘⟨ *-congˡ (×-assoc-* (n C k) _ _) ⟩
+      x * ((n C k) × x ^ k * y ^ (n ∸ k))         ≈˘⟨ *-assoc x ((n C k) × x ^ k) _ ⟩
+      (x * (n C k) × x ^ k) * y ^ (n ∸ k)         ≈⟨ *-congʳ (×-comm-* (n C k) _ _) ⟩
+      (n C k) × x ^ (suc k) * y ^ (n ∸ k)         ≡⟨⟩
+      (n C k) × x ^ (suc k) * y ^ (suc n ∸ suc k) ≈⟨ ×-assoc-* (n C k) _ _ ⟩
+      (n C k) × Binomial.binomial (suc n) (suc i) ∎
+      where
+        open ≈-Reasoning
+        k = toℕ i
+
+    
+------------------------------------------------------------------------
+-- Next, a lemma which does require commutativity
+
+  module _ (x*y≈y*x : x * y ≈ y * x) where
+  
+    module _ (n : ℕ) where 
+
+      open Binomial n using (binomial; term; term₁; term₂)
+
+      y*lemma : (j : Fin n) → let i = inject₁ j in
+        y * term (suc j) ≈ (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i)
+      y*lemma j = begin
+        y * term (suc j)
+          ≈⟨ ×-comm-* nC[j+1] y (binomial (suc j)) ⟩
+        nC[j+1] × (y * binomial (suc j))
+          ≈⟨ ×-congʳ nC[j+1] (y*x^m*y^n≈x^m*y^[n+1] x*y≈y*x [j+1] [n-j-1]) ⟩
+        nC[j+1] × (x ^ [j+1] * y ^ [n-j])
+          ≈˘⟨ ×-congʳ nC[j+1] (*-congʳ (^-congʳ x [k+1]≡[j+1])) ⟩
+        nC[j+1] × (x ^ [k+1] * y ^ [n-j])
+          ≈˘⟨ ×-congʳ nC[j+1] (*-congˡ (^-congʳ y [n-k]≡[n-j])) ⟩
+        nC[j+1] × (x ^ [k+1] * y ^ [n-k])
+          ≡⟨⟩
+        nC[j+1] × (x ^ [k+1] * y ^ [n+1]-[k+1])
+          ≡⟨⟩
+        (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i) ∎
+        where
+          i           = inject₁ j
+          k           = toℕ i
+          k≡j         : k ≡ toℕ j
+          k≡j         = toℕ-inject₁ j
+          
+          [k+1]       = ℕ.suc k
+          [j+1]       = toℕ (suc j)
+          [n-k]       = n ∸ k
+          [n+1]-[k+1] = [n-k]
+          [n-j-1]     = n ∸ [j+1]
+          [n-j]       = ℕ.suc [n-j-1]
+          nC[j+1]     = n C [j+1]
+
+          [k+1]≡[j+1] : [k+1] ≡ [j+1]
+          [k+1]≡[j+1] = cong suc k≡j
+          
+          [n-k]≡[n-j] : [n-k] ≡ [n-j]
+          [n-k]≡[n-j] = begin 
+            [n-k]       ≡⟨ cong (n ∸_) k≡j ⟩
+            n ∸ toℕ j  ≡˘⟨ [m-n-1]+1≡[m-n] (toℕ<n j) ⟩
+            [n-j]       ∎ where open ≡-Reasoning
+          open ≈-Reasoning
+            
+------------------------------------------------------------------------
+-- Now, a lemma characterising the sum of the term₁ and term₂ expressions
+
+      open ≈-Reasoning
+
+      lemma₁₊₂₌ₑₓₚ : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
+      
+      lemma₁₊₂₌ₑₓₚ 0F = begin
+        term₁ 0F + term₂ 0F          ≡⟨⟩
+        0# + y * (1 × (1# * y ^ n))  ≈⟨ +-identityˡ _ ⟩
+        y * (1 × (1# * y ^ n))       ≈⟨ *-congˡ (+-identityʳ (1# * y ^ n)) ⟩
+        y * (1# * y ^ n)             ≈⟨ *-congˡ (*-identityˡ (y ^ n)) ⟩
+        y * y ^ n                    ≡⟨⟩
+        y ^ suc n                    ≈˘⟨ *-identityˡ (y ^ suc n) ⟩
+        1# * y ^ suc n               ≈˘⟨ +-identityʳ (1# * y ^ suc n) ⟩
+        1 × (1# * y ^ suc n)         ≡⟨⟩
+        Binomial.term (suc n) 0F      ∎
+
+      lemma₁₊₂₌ₑₓₚ (suc i) with view i
+      ... | top
+      {- remembering that i = fromℕ n, definitionally -}
+        rewrite view-top-toℕ i {{Instances.top⁺}}
+          | nCn≡1 n
+          | n∸n≡0 n
+          | n<ᵇ1+n n
+          = begin
+        x * ((x ^ n * 1#) + 0#) + 0# ≈⟨ +-identityʳ _ ⟩
+        x * ((x ^ n * 1#) + 0#)      ≈⟨ *-congˡ (+-identityʳ _) ⟩
+        x * (x ^ n * 1#)             ≈˘⟨ *-assoc _ _ _ ⟩
+        x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
+        1 × (x * x ^ n * 1#)         ∎
+
+      ... | inj j
+      {- remembering that i = inject₁ j, definitionally -}
+          = begin
+        (x * term i) + (y * term (suc j))
+          ≈⟨ +-cong (x*lemma i) (y*lemma j) ⟩
+        (nCk × [x^k+1]*[y^n-k]) + (nC[j+1] × [x^k+1]*[y^n-k])
+          ≈˘⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟩  
+        (nCk × [x^k+1]*[y^n-k]) + (nC[k+1] × [x^k+1]*[y^n-k])
+          ≈˘⟨ ×-homo-+ [x^k+1]*[y^n-k] nCk nC[k+1] ⟩
+        (nCk Nat.+ nC[k+1]) × [x^k+1]*[y^n-k]
+          ≡⟨ cong (_× [x^k+1]*[y^n-k]) (nCk+nC[k+1]≡[n+1]C[k+1] n k) ⟩
+        ((suc n) C (suc k)) × [x^k+1]*[y^n-k]
+          ≡⟨⟩
+        Binomial.term (suc n) (suc i) ∎
+          where
+            k               = toℕ i
+            [k+1]           = ℕ.suc k
+            [j+1]           = toℕ (suc j)
+            nCk             = n C k
+            nC[k+1]         = n C [k+1]
+            nC[j+1]         = n C [j+1]
+            nC[k+1]≡nC[j+1] : nC[k+1] ≡ nC[j+1]
+            nC[k+1]≡nC[j+1] = cong ((n C_) ∘ suc) (toℕ-inject₁ j)
+            [x^k+1]*[y^n-k] : Carrier
+            [x^k+1]*[y^n-k] = Binomial.binomial (suc n) (suc i)
+
+------------------------------------------------------------------------
+-- Finally, the main result
+
+    open ≈-Reasoning
+    
+    theorem : ∀ n → ((x + y) ^ n) ≈ Binomial.expansion n
+  
+    theorem zero    = begin
+      (x + y) ^ 0                     ≡⟨⟩
+      1#                              ≈˘⟨ 1×-identityʳ 1# ⟩
+      1 × 1#                          ≈˘⟨ *-identityʳ (1 × 1#) ⟩
+      (1 × 1#) * 1#                   ≈⟨ ×-assoc-* 1 1# 1# ⟩
+      1 × (1# * 1#)                   ≡⟨⟩
+      1 × (x ^ 0 * y ^ 0)             ≈˘⟨ +-identityʳ _ ⟩
+      1 × (x ^ 0 * y ^ 0) + 0#        ≡⟨⟩
+      (0 C 0) × (x ^ 0 * y ^ 0) + 0#  ≡⟨⟩
+      Binomial.expansion 0            ∎
+
+    theorem n@(suc n-1) = begin
+      (x + y) ^ n                         ≡⟨⟩
+      (x + y) * (x + y) ^ n-1             ≈⟨ *-congˡ (theorem n-1) ⟩
+      (x + y) * expansion                 ≈⟨ distribʳ _ _ _ ⟩
+      x * expansion + y * expansion       ≈⟨ +-cong lemma₁ lemma₂ ⟩
+      sum₁ + sum₂                         ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
+      ∑[ i < suc n ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (lemma₁₊₂₌ₑₓₚ n-1) ⟩
+      ∑[ i < suc n ] Binomial.term n i    ≡⟨⟩
+      Binomial.expansion n                ∎
+      where
+        open Binomial n-1
+        open BinomialLemmas n-1
+

From 5e934918843035c8be9de0a74f8452a2857dddfa Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 11 May 2023 15:29:14 +0100
Subject: [PATCH 02/19] followed Nathan's suggestions; fixed up dependencies;
 rebase and recheck

---
 src/Algebra/Properties/Semiring/Binomial.agda | 53 +++++++++++++------
 1 file changed, 36 insertions(+), 17 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 671b209bf2..c0c4892c65 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -7,11 +7,12 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Bundles using (Semiring)
+open import Data.Bool.Base using (true; false)
 open import Data.Nat.Base as Nat hiding (_+_; _*_; _^_)
 open import Data.Nat.Combinatorics
   using (_C_; nCn≡1; nC1≡n; nCk+nC[k+1]≡[n+1]C[k+1])
 open import Data.Nat.Properties as Nat
-  using (n<ᵇ1+n; n∸n≡0; [m-n-1]+1≡[m-n])
+  using (<⇒<ᵇ; n<1+n; n∸n≡0; +-∸-assoc)
 open import Data.Fin.Base as Fin
   using (Fin; zero; suc; toℕ; fromℕ; inject₁)
 open import Data.Fin.Patterns using (0F)
@@ -22,6 +23,7 @@ open import Data.Fin.Relation.Unary.TopView
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; cong; module ≡-Reasoning)
+  renaming (refl to ≡-refl)
 
 module Algebra.Properties.Semiring.Binomial {a ℓ} (S : Semiring a ℓ) where
 
@@ -105,7 +107,7 @@ module _ (x y : Carrier) where
       ∑[ i < suc n ] (y * term i) + 0#
         ≈⟨ +-cong (sum-cong-≋ lemma₂-inj) lemma₂-top ⟩
       (∑[ i < suc n ] term₂-inj i) + term₂ [n+1]
-        ≈˘⟨ sum-init term₂ ⟩
+        ≈˘⟨ sum-init-last term₂ ⟩
       sum term₂
         ≡⟨⟩
       sum₂  ∎
@@ -128,7 +130,11 @@ module _ (x y : Carrier) where
 
     open Binomial n using (term)
 
-    x*lemma : x * term i ≈ (n C toℕ i) × Binomial.binomial (suc n) (suc i)
+    private
+
+      k = toℕ i
+
+    x*lemma : x * term i ≈ (n C k) × Binomial.binomial (suc n) (suc i)
     x*lemma = begin
       x * term i                                  ≡⟨⟩
       x * ((n C k) × (x ^ k * y ^ (n ∸ k)))       ≈˘⟨ *-congˡ (×-assoc-* (n C k) _ _) ⟩
@@ -139,7 +145,7 @@ module _ (x y : Carrier) where
       (n C k) × Binomial.binomial (suc n) (suc i) ∎
       where
         open ≈-Reasoning
-        k = toℕ i
+        
 
     
 ------------------------------------------------------------------------
@@ -147,13 +153,16 @@ module _ (x y : Carrier) where
 
   module _ (x*y≈y*x : x * y ≈ y * x) where
   
-    module _ (n : ℕ) where 
+    module _ {n : ℕ} (j : Fin n) where 
+
+      open Binomial n using (binomial; term)
 
-      open Binomial n using (binomial; term; term₁; term₂)
+      private
+
+        i = inject₁ j
 
-      y*lemma : (j : Fin n) → let i = inject₁ j in
-        y * term (suc j) ≈ (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i)
-      y*lemma j = begin
+      y*lemma : y * term (suc j) ≈ (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i)
+      y*lemma = begin
         y * term (suc j)
           ≈⟨ ×-comm-* nC[j+1] y (binomial (suc j)) ⟩
         nC[j+1] × (y * binomial (suc j))
@@ -168,7 +177,6 @@ module _ (x y : Carrier) where
           ≡⟨⟩
         (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i) ∎
         where
-          i           = inject₁ j
           k           = toℕ i
           k≡j         : k ≡ toℕ j
           k≡j         = toℕ-inject₁ j
@@ -187,18 +195,29 @@ module _ (x y : Carrier) where
           [n-k]≡[n-j] : [n-k] ≡ [n-j]
           [n-k]≡[n-j] = begin 
             [n-k]       ≡⟨ cong (n ∸_) k≡j ⟩
-            n ∸ toℕ j  ≡˘⟨ [m-n-1]+1≡[m-n] (toℕ<n j) ⟩
+            n ∸ toℕ j  ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟩
             [n-j]       ∎ where open ≡-Reasoning
           open ≈-Reasoning
             
 ------------------------------------------------------------------------
 -- Now, a lemma characterising the sum of the term₁ and term₂ expressions
 
+    module _ n where
+  
       open ≈-Reasoning
 
-      lemma₁₊₂₌ₑₓₚ : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
+      open Binomial n using (term; term₁; term₂)
+
+      private
+
+        n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
+        n<ᵇ1+n with n Nat.<ᵇ suc n in eq | <⇒<ᵇ (n<1+n n)
+        ... | true | _ = ≡-refl
+
+
+      term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
       
-      lemma₁₊₂₌ₑₓₚ 0F = begin
+      term₁+term₂≈term 0F = begin
         term₁ 0F + term₂ 0F          ≡⟨⟩
         0# + y * (1 × (1# * y ^ n))  ≈⟨ +-identityˡ _ ⟩
         y * (1 × (1# * y ^ n))       ≈⟨ *-congˡ (+-identityʳ (1# * y ^ n)) ⟩
@@ -209,20 +228,20 @@ module _ (x y : Carrier) where
         1 × (1# * y ^ suc n)         ≡⟨⟩
         Binomial.term (suc n) 0F      ∎
 
-      lemma₁₊₂₌ₑₓₚ (suc i) with view i
+      term₁+term₂≈term (suc i) with view i
       ... | top
       {- remembering that i = fromℕ n, definitionally -}
         rewrite view-top-toℕ i {{Instances.top⁺}}
           | nCn≡1 n
           | n∸n≡0 n
-          | n<ᵇ1+n n
+          | n<ᵇ1+n
           = begin
         x * ((x ^ n * 1#) + 0#) + 0# ≈⟨ +-identityʳ _ ⟩
         x * ((x ^ n * 1#) + 0#)      ≈⟨ *-congˡ (+-identityʳ _) ⟩
         x * (x ^ n * 1#)             ≈˘⟨ *-assoc _ _ _ ⟩
         x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
         1 × (x * x ^ n * 1#)         ∎
-
+ 
       ... | inj j
       {- remembering that i = inject₁ j, definitionally -}
           = begin
@@ -273,7 +292,7 @@ module _ (x y : Carrier) where
       (x + y) * expansion                 ≈⟨ distribʳ _ _ _ ⟩
       x * expansion + y * expansion       ≈⟨ +-cong lemma₁ lemma₂ ⟩
       sum₁ + sum₂                         ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
-      ∑[ i < suc n ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (lemma₁₊₂₌ₑₓₚ n-1) ⟩
+      ∑[ i < suc n ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n-1) ⟩
       ∑[ i < suc n ] Binomial.term n i    ≡⟨⟩
       Binomial.expansion n                ∎
       where

From 434546f99d75b2d096c0859c4b2ed24ff8d1fbe6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 11 May 2023 15:34:09 +0100
Subject: [PATCH 03/19] `--cubica-compatible` plus fix-whitespace

---
 .../CommutativeSemiring/Binomial.agda         |  6 +---
 src/Algebra/Properties/Semiring/Binomial.agda | 32 +++++++++----------
 2 files changed, 17 insertions(+), 21 deletions(-)

diff --git a/src/Algebra/Properties/CommutativeSemiring/Binomial.agda b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
index 6527e6f862..688dc8978f 100644
--- a/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
+++ b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
@@ -4,7 +4,7 @@
 -- The Binomial Theorem for Commutative Semirings
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles
   using (CommutativeSemiring)
@@ -22,7 +22,3 @@ open Binomial public hiding (theorem)
 theorem : ∀ n x y → ((x + y) ^ n) ≈ Binomial.expansion x y n
 theorem n x y = Binomial.theorem x y (*-comm x y) n
 
-
-
-
-
diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index c0c4892c65..d5ea3c7799 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -4,10 +4,10 @@
 -- The Binomial Theorem for *-commuting elements in a Semiring
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Semiring)
-open import Data.Bool.Base using (true; false)
+open import Data.Bool.Base using (true)
 open import Data.Nat.Base as Nat hiding (_+_; _*_; _^_)
 open import Data.Nat.Combinatorics
   using (_C_; nCn≡1; nC1≡n; nCk+nC[k+1]≡[n+1]C[k+1])
@@ -145,15 +145,15 @@ module _ (x y : Carrier) where
       (n C k) × Binomial.binomial (suc n) (suc i) ∎
       where
         open ≈-Reasoning
-        
 
-    
+
+
 ------------------------------------------------------------------------
 -- Next, a lemma which does require commutativity
 
   module _ (x*y≈y*x : x * y ≈ y * x) where
-  
-    module _ {n : ℕ} (j : Fin n) where 
+
+    module _ {n : ℕ} (j : Fin n) where
 
       open Binomial n using (binomial; term)
 
@@ -180,7 +180,7 @@ module _ (x y : Carrier) where
           k           = toℕ i
           k≡j         : k ≡ toℕ j
           k≡j         = toℕ-inject₁ j
-          
+
           [k+1]       = ℕ.suc k
           [j+1]       = toℕ (suc j)
           [n-k]       = n ∸ k
@@ -191,19 +191,19 @@ module _ (x y : Carrier) where
 
           [k+1]≡[j+1] : [k+1] ≡ [j+1]
           [k+1]≡[j+1] = cong suc k≡j
-          
+
           [n-k]≡[n-j] : [n-k] ≡ [n-j]
-          [n-k]≡[n-j] = begin 
+          [n-k]≡[n-j] = begin
             [n-k]       ≡⟨ cong (n ∸_) k≡j ⟩
             n ∸ toℕ j  ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟩
             [n-j]       ∎ where open ≡-Reasoning
           open ≈-Reasoning
-            
+
 ------------------------------------------------------------------------
 -- Now, a lemma characterising the sum of the term₁ and term₂ expressions
 
     module _ n where
-  
+
       open ≈-Reasoning
 
       open Binomial n using (term; term₁; term₂)
@@ -216,7 +216,7 @@ module _ (x y : Carrier) where
 
 
       term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
-      
+
       term₁+term₂≈term 0F = begin
         term₁ 0F + term₂ 0F          ≡⟨⟩
         0# + y * (1 × (1# * y ^ n))  ≈⟨ +-identityˡ _ ⟩
@@ -241,14 +241,14 @@ module _ (x y : Carrier) where
         x * (x ^ n * 1#)             ≈˘⟨ *-assoc _ _ _ ⟩
         x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
         1 × (x * x ^ n * 1#)         ∎
- 
+
       ... | inj j
       {- remembering that i = inject₁ j, definitionally -}
           = begin
         (x * term i) + (y * term (suc j))
           ≈⟨ +-cong (x*lemma i) (y*lemma j) ⟩
         (nCk × [x^k+1]*[y^n-k]) + (nC[j+1] × [x^k+1]*[y^n-k])
-          ≈˘⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟩  
+          ≈˘⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟩
         (nCk × [x^k+1]*[y^n-k]) + (nC[k+1] × [x^k+1]*[y^n-k])
           ≈˘⟨ ×-homo-+ [x^k+1]*[y^n-k] nCk nC[k+1] ⟩
         (nCk Nat.+ nC[k+1]) × [x^k+1]*[y^n-k]
@@ -272,9 +272,9 @@ module _ (x y : Carrier) where
 -- Finally, the main result
 
     open ≈-Reasoning
-    
+
     theorem : ∀ n → ((x + y) ^ n) ≈ Binomial.expansion n
-  
+
     theorem zero    = begin
       (x + y) ^ 0                     ≡⟨⟩
       1#                              ≈˘⟨ 1×-identityʳ 1# ⟩

From d6cc72b6b734112ca6c984a9fe2aac2d8225a833 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 11 May 2023 15:48:10 +0100
Subject: [PATCH 04/19] clean copy of `Top` view

---
 src/Algebra/Properties/Semiring/Binomial.agda |   2 +-
 src/Data/Fin/Relation/Unary/Top.agda          | 141 ++++++++++++++++++
 2 files changed, 142 insertions(+), 1 deletion(-)
 create mode 100644 src/Data/Fin/Relation/Unary/Top.agda

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index d5ea3c7799..790dc7ec48 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -18,7 +18,7 @@ open import Data.Fin.Base as Fin
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties as Fin
   using (toℕ<n; toℕ-inject₁)
-open import Data.Fin.Relation.Unary.TopView
+open import Data.Fin.Relation.Unary.Top
   using (view; top; inj; view-inj; view-top; view-top-toℕ; module Instances)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda
new file mode 100644
index 0000000000..d24d2fd826
--- /dev/null
+++ b/src/Data/Fin/Relation/Unary/Top.agda
@@ -0,0 +1,141 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The 'top' view of Fin
+--
+-- This is an example of a view of (elements of) a datatype,
+-- here i : Fin (suc n), which exhibits every such i as
+-- * either, i = fromℕ n
+-- * or, i = inject₁ j for a unique j : Fin n
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Relation.Unary.Top where
+
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_)
+open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc)
+open import Data.Product using (uncurry)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Fin.Base hiding (_<_)
+open import Data.Fin.Properties as Fin
+  using (suc-injective; toℕ-fromℕ; toℕ<n; toℕ-inject₁; inject₁ℕ<)
+open import Relation.Binary.PropositionalEquality
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- The View, considered as a unary relation on Fin (suc n)
+
+-- First, a lemma not in `Data.Fin.Properties`,
+-- but which establishes disjointness of the
+-- (interpretations of the) constructors of the View
+
+top≢inject₁ : ∀ (j : Fin n) → fromℕ n ≢ inject₁ j
+top≢inject₁ (suc j) eq = top≢inject₁ j (suc-injective eq)
+
+-- The View, itself
+
+data View : (i : Fin (suc n)) → Set where
+
+  top :                View (fromℕ n)
+  inj : (j : Fin n) → View (inject₁ j)
+
+-- The view covering function, witnessing soundness of the view
+
+view : ∀ {n} i → View {n} i
+view {n = zero}  zero = top
+view {n = suc _} zero = inj _
+view {n = suc n} (suc i) with view {n} i
+... | top   = top
+... | inj j = inj (suc j)
+
+-- Interpretation of the view constructors
+
+⟦_⟧ : ∀ {i} → View {n} i → Fin (suc n)
+⟦ top ⟧   = fromℕ _
+⟦ inj j ⟧ = inject₁ j
+
+-- Completeness of the view
+
+view-complete : ∀ {i} (v : View {n} i) → ⟦ v ⟧ ≡ i
+view-complete top     = refl
+view-complete (inj j) = refl
+
+-- 'Computational' behaviour of the covering function
+
+view-top : ∀ n → view {n} (fromℕ n) ≡ top
+view-top zero    = refl
+view-top (suc n) rewrite view-top n = refl
+
+view-inj : ∀ j → view {n} (inject₁ j) ≡ inj j
+view-inj zero       = refl
+view-inj (suc j) rewrite view-inj j = refl
+
+------------------------------------------------------------------------
+-- Experimental
+--
+-- Because we work --without-K, Agda's unifier will complain about
+-- attempts to match `refl` against hypotheses of the form
+--    `view {n] i ≡ v`
+-- or gets stuck trying to solve unification problems of the form
+--    (inferred index ≟ expected index)
+-- even when these problems are *provably* solvable.
+--
+-- So the two predicates on values of the view defined below
+-- are extensionally equivalent to the assertions
+-- `view {n] i ≡ top` and `view {n] i ≡ inj j`
+--
+-- But such assertions can only ever have a unique (irrelevant) proof
+-- so we introduce instances to witness them, themselves given by
+-- the functions `view-top` and `view-inj` defined above
+
+module Instances {n} where
+
+  data IsTop : ∀ {i} → View {n} i → Set where
+
+    top : IsTop top
+
+  instance
+
+    top⁺ : IsTop {i = fromℕ n} (view (fromℕ n))
+    top⁺ rewrite view-top n = top
+
+  data IsInj : ∀ {i} → View {n} i → Set where
+
+    inj : ∀ j → IsInj (inj j)
+
+  instance
+
+    inj⁺ : ∀ {j} → IsInj (view (inject₁ j))
+    inj⁺ {j} rewrite view-inj j = inj j
+
+    inject₁≡⁺ : ∀ {i} {j} {eq : inject₁ i ≡ j} → IsInj (view j)
+    inject₁≡⁺ {eq = refl} = inj⁺
+
+    n≢inject₁⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view i)
+    n≢inject₁⁺ {i} {n≢i} with view i
+    ... | top   = ⊥-elim (n≢i (begin
+      n                         ≡˘⟨ toℕ-fromℕ n ⟩
+      toℕ (fromℕ n)           ≡˘⟨ toℕ-inject₁ (fromℕ n) ⟩
+      toℕ (inject₁ (fromℕ n)) ∎)) where open ≡-Reasoning
+    ... | inj j = inj j
+
+open Instances
+
+------------------------------------------------------------------------
+-- As a corollary, we obtain two useful properties, which are
+-- witnessed by, but can also serve as proxy replacements for,
+-- the corresponding properties in `Data.Fin.Properties`
+
+module _ {n} where
+
+  view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n
+  view-top-toℕ i with top ← view i = toℕ-fromℕ n
+
+  view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n
+  view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j
+

From 54fdf952886f2ab110eb2f62a160de54b24e70f1 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 11 May 2023 15:51:34 +0100
Subject: [PATCH 05/19] updated `CHANGELOG` with `Top` view

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 17ef715fc7..efe671ed2d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1402,6 +1402,11 @@ New modules
   Data.Default
   ```
 
+* A small library defining a structurally inductive view of `Fin (suc n)`:
+  ```
+  Data.Fin.Relation.Unary.Top
+  ```
+
 * A small library for a non-empty fresh list:
   ```
   Data.List.Fresh.NonEmpty

From a16a15f234f176bd065028f5b7b060950cfba930 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 12 May 2023 08:33:35 +0100
Subject: [PATCH 06/19] review changes

---
 src/Data/Fin/Relation/Unary/Top.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda
index d24d2fd826..3b99ff90a4 100644
--- a/src/Data/Fin/Relation/Unary/Top.agda
+++ b/src/Data/Fin/Relation/Unary/Top.agda
@@ -78,7 +78,7 @@ view-inj (suc j) rewrite view-inj j = refl
 ------------------------------------------------------------------------
 -- Experimental
 --
--- Because we work --without-K, Agda's unifier will complain about
+-- Because we work without K, Agda's unifier will complain about
 -- attempts to match `refl` against hypotheses of the form
 --    `view {n] i ≡ v`
 -- or gets stuck trying to solve unification problems of the form

From 809c1158c4f3aaebe3fabfefad3d17bd2adc7707 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Aug 2023 14:14:49 +0100
Subject: [PATCH 07/19] minor simplification

---
 src/Algebra/Properties/Semiring/Binomial.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 790dc7ec48..c5f56a775e 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -211,7 +211,7 @@ module _ (x y : Carrier) where
       private
 
         n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
-        n<ᵇ1+n with n Nat.<ᵇ suc n in eq | <⇒<ᵇ (n<1+n n)
+        n<ᵇ1+n with n Nat.<ᵇ suc n | <⇒<ᵇ (n<1+n n)
         ... | true | _ = ≡-refl
 
 

From 9b1106473c3574b6a3ddf1204719b8203148a70e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Aug 2023 14:26:59 +0100
Subject: [PATCH 08/19] cosmetic tweaks

---
 src/Algebra/Properties/Semiring/Binomial.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index c5f56a775e..bd69e86401 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -194,9 +194,9 @@ module _ (x y : Carrier) where
 
           [n-k]≡[n-j] : [n-k] ≡ [n-j]
           [n-k]≡[n-j] = begin
-            [n-k]       ≡⟨ cong (n ∸_) k≡j ⟩
+            [n-k]      ≡⟨ cong (n ∸_) k≡j ⟩
             n ∸ toℕ j  ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟩
-            [n-j]       ∎ where open ≡-Reasoning
+            [n-j]      ∎ where open ≡-Reasoning
           open ≈-Reasoning
 
 ------------------------------------------------------------------------
@@ -226,7 +226,7 @@ module _ (x y : Carrier) where
         y ^ suc n                    ≈˘⟨ *-identityˡ (y ^ suc n) ⟩
         1# * y ^ suc n               ≈˘⟨ +-identityʳ (1# * y ^ suc n) ⟩
         1 × (1# * y ^ suc n)         ≡⟨⟩
-        Binomial.term (suc n) 0F      ∎
+        Binomial.term (suc n) 0F     ∎
 
       term₁+term₂≈term (suc i) with view i
       ... | top

From 73db427dbfecfe425a0c9d1bf8e6aa757427a3d7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Aug 2023 15:27:20 +0100
Subject: [PATCH 09/19] removed dependency on `Top.Instances`

---
 src/Algebra/Properties/Semiring/Binomial.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index bd69e86401..1414b02794 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -17,9 +17,9 @@ open import Data.Fin.Base as Fin
   using (Fin; zero; suc; toℕ; fromℕ; inject₁)
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties as Fin
-  using (toℕ<n; toℕ-inject₁)
+  using (toℕ<n; toℕ-fromℕ; toℕ-inject₁)
 open import Data.Fin.Relation.Unary.Top
-  using (view; top; inj; view-inj; view-top; view-top-toℕ; module Instances)
+  using (view; top; inj; view-inj; view-top)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; cong; module ≡-Reasoning)
@@ -231,7 +231,7 @@ module _ (x y : Carrier) where
       term₁+term₂≈term (suc i) with view i
       ... | top
       {- remembering that i = fromℕ n, definitionally -}
-        rewrite view-top-toℕ i {{Instances.top⁺}}
+        rewrite toℕ-fromℕ n
           | nCn≡1 n
           | n∸n≡0 n
           | n<ᵇ1+n

From f3bebb57000a78a91cec80287ac43a6eb265c03b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 11:20:27 +0100
Subject: [PATCH 10/19] tightened imports

---
 src/Algebra/Properties/Semiring/Binomial.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 1414b02794..98715868dd 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -21,7 +21,7 @@ open import Data.Fin.Properties as Fin
 open import Data.Fin.Relation.Unary.Top
   using (view; top; inj; view-inj; view-top)
 open import Function.Base using (_∘_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; cong; module ≡-Reasoning)
   renaming (refl to ≡-refl)
 

From 2942b081ec7afe36ae86524bbd34d6c5b9f0888a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 11:24:07 +0100
Subject: [PATCH 11/19] moved `Top` to `TopBinomial` for subsequent deletion
 after merging #1923

---
 src/Algebra/Properties/Semiring/Binomial.agda              | 2 +-
 src/Data/Fin/Relation/Unary/{Top.agda => TopBinomial.agda} | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)
 rename src/Data/Fin/Relation/Unary/{Top.agda => TopBinomial.agda} (98%)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 98715868dd..47eaa0856b 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -18,7 +18,7 @@ open import Data.Fin.Base as Fin
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties as Fin
   using (toℕ<n; toℕ-fromℕ; toℕ-inject₁)
-open import Data.Fin.Relation.Unary.Top
+open import Data.Fin.Relation.Unary.TopBinomial
   using (view; top; inj; view-inj; view-top)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/TopBinomial.agda
similarity index 98%
rename from src/Data/Fin/Relation/Unary/Top.agda
rename to src/Data/Fin/Relation/Unary/TopBinomial.agda
index 3b99ff90a4..68bf9f9fdf 100644
--- a/src/Data/Fin/Relation/Unary/Top.agda
+++ b/src/Data/Fin/Relation/Unary/TopBinomial.agda
@@ -11,13 +11,12 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.Fin.Relation.Unary.Top where
+module Data.Fin.Relation.Unary.TopBinomial where
 
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_)
 open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc)
 open import Data.Product using (uncurry)
-open import Data.Sum using (inj₁; inj₂)
 open import Data.Fin.Base hiding (_<_)
 open import Data.Fin.Properties as Fin
   using (suc-injective; toℕ-fromℕ; toℕ<n; toℕ-inject₁; inject₁ℕ<)

From 81679a578aed2402dda9bb5ad8a96f3d7366a6d8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 11:31:31 +0100
Subject: [PATCH 12/19] more tweaks to private lemma

---
 src/Algebra/Properties/Semiring/Binomial.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 47eaa0856b..b465a75404 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -211,8 +211,7 @@ module _ (x y : Carrier) where
       private
 
         n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
-        n<ᵇ1+n with n Nat.<ᵇ suc n | <⇒<ᵇ (n<1+n n)
-        ... | true | _ = ≡-refl
+        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = {!≡-refl!}
 
 
       term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i

From 249a772cb9cdf5c7bd18726b40825a5da11e835c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 11:49:05 +0100
Subject: [PATCH 13/19] pushed before saving

---
 src/Algebra/Properties/Semiring/Binomial.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index b465a75404..e7fff1bafb 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -211,7 +211,7 @@ module _ (x y : Carrier) where
       private
 
         n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
-        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = {!≡-refl!}
+        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡-refl
 
 
       term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i

From e20d47e112d8846bd7a7f162a387f7adfe05fde5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 13:01:22 +0100
Subject: [PATCH 14/19] cosmetic tweaks to final proof

---
 src/Algebra/Properties/Semiring/Binomial.agda | 22 +++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index e7fff1bafb..deb111a6d4 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -285,16 +285,16 @@ module _ (x y : Carrier) where
       (0 C 0) × (x ^ 0 * y ^ 0) + 0#  ≡⟨⟩
       Binomial.expansion 0            ∎
 
-    theorem n@(suc n-1) = begin
-      (x + y) ^ n                         ≡⟨⟩
-      (x + y) * (x + y) ^ n-1             ≈⟨ *-congˡ (theorem n-1) ⟩
-      (x + y) * expansion                 ≈⟨ distribʳ _ _ _ ⟩
-      x * expansion + y * expansion       ≈⟨ +-cong lemma₁ lemma₂ ⟩
-      sum₁ + sum₂                         ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
-      ∑[ i < suc n ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n-1) ⟩
-      ∑[ i < suc n ] Binomial.term n i    ≡⟨⟩
-      Binomial.expansion n                ∎
+    theorem n+1@(suc n) = begin
+      (x + y) ^ n+1                         ≡⟨⟩
+      (x + y) * (x + y) ^ n                 ≈⟨ *-congˡ (theorem n) ⟩
+      (x + y) * expansion                   ≈⟨ distribʳ _ _ _ ⟩
+      x * expansion + y * expansion         ≈⟨ +-cong lemma₁ lemma₂ ⟩
+      sum₁ + sum₂                           ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
+      ∑[ i < suc n+1 ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n) ⟩
+      ∑[ i < suc n+1 ] Binomial.term n+1 i  ≡⟨⟩
+      Binomial.expansion n+1                ∎
       where
-        open Binomial n-1
-        open BinomialLemmas n-1
+        open Binomial n
+        open BinomialLemmas n
 

From 699b00c362ef4710d7d715786a790a2cf9d07466 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 8 Aug 2023 13:20:25 +0100
Subject: [PATCH 15/19] added more syntax for sums

---
 CHANGELOG.md                                  |  2 +-
 src/Algebra/Properties/Monoid/Sum.agda        |  6 +++-
 src/Algebra/Properties/Semiring/Binomial.agda | 34 +++++++++----------
 3 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index efe671ed2d..8b1642590d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1769,7 +1769,7 @@ Other minor changes
 
 * Added new proof to `Algebra.Properties.Monoid.Sum`:
   ```agda
-  sum-init-last : ∀ {n} (t : Vector _ (suc n)) → sum t ≈ sum (init t) + last t
+  sum-init-last : (t : Vector _ (suc n)) → sum t ≈ sum (init t) + last t
   ```
 
 * Added new proofs to `Algebra.Properties.Semigroup`:
diff --git a/src/Algebra/Properties/Monoid/Sum.agda b/src/Algebra/Properties/Monoid/Sum.agda
index 1f522ca678..26c3effd6a 100644
--- a/src/Algebra/Properties/Monoid/Sum.agda
+++ b/src/Algebra/Properties/Monoid/Sum.agda
@@ -42,13 +42,17 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
 ------------------------------------------------------------------------
 -- An alternative mathematical-style syntax for sumₜ
 
-infixl 10 sum-syntax
+infixl 10 sum-syntax sum⁺-syntax
 
 sum-syntax : ∀ n → Vector Carrier n → Carrier
 sum-syntax _ = sum
 
 syntax sum-syntax n (λ i → x) = ∑[ i < n ] x
 
+sum⁺-syntax = sum-syntax ∘ suc
+
+syntax sum⁺-syntax n (λ i → x) = ∑[ i ≤ n ] x
+
 ------------------------------------------------------------------------
 -- Properties
 
diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index deb111a6d4..655e864f18 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -60,14 +60,14 @@ module _ (x y : Carrier) where
       term = (n C k) × binomial
 
     expansion : Carrier
-    expansion = ∑[ i < suc n ] term i
+    expansion = ∑[ i ≤ n ] term i
 
     term₁ : (i : Fin (suc (suc n))) → Carrier
     term₁ zero    = 0#
     term₁ (suc i) = x * term i
 
     sum₁ : Carrier
-    sum₁ = ∑[ i < suc (suc n) ] term₁ i
+    sum₁ = ∑[ i ≤ suc n ] term₁ i
 
     term₂ : (i : Fin (suc (suc n))) → Carrier
     term₂ i with view i
@@ -75,7 +75,7 @@ module _ (x y : Carrier) where
     ... | inj j = y * term j
 
     sum₂ : Carrier
-    sum₂ = ∑[ i < suc (suc n) ] term₂ i
+    sum₂ = ∑[ i ≤ suc n ] term₂ i
 
 ------------------------------------------------------------------------
 -- Properties
@@ -90,11 +90,11 @@ module _ (x y : Carrier) where
     lemma₁ = begin
       x * expansion
         ≈⟨ *-distribˡ-sum x term ⟩
-      ∑[ i < suc n ] (x * term i)
+      ∑[ i ≤ n ] (x * term i)
         ≈˘⟨ +-identityˡ _ ⟩
-      (0# + ∑[ i < suc n ] (x * term i))
+      (0# + ∑[ i ≤ n ] (x * term i))
         ≡⟨⟩
-      (0# + ∑[ i < suc n ] term₁ (suc i))
+      (0# + ∑[ i ≤ n ] term₁ (suc i))
         ≡⟨⟩
       sum₁  ∎
 
@@ -102,11 +102,11 @@ module _ (x y : Carrier) where
     lemma₂ = begin
       (y * expansion)
         ≈⟨ *-distribˡ-sum y term ⟩
-      ∑[ i < suc n ] (y * term i)
+      ∑[ i ≤ n ] (y * term i)
         ≈˘⟨ +-identityʳ _ ⟩
-      ∑[ i < suc n ] (y * term i) + 0#
+      ∑[ i ≤ n ] (y * term i) + 0#
         ≈⟨ +-cong (sum-cong-≋ lemma₂-inj) lemma₂-top ⟩
-      (∑[ i < suc n ] term₂-inj i) + term₂ [n+1]
+      (∑[ i ≤ n ] term₂-inj i) + term₂ [n+1]
         ≈˘⟨ sum-init-last term₂ ⟩
       sum term₂
         ≡⟨⟩
@@ -286,14 +286,14 @@ module _ (x y : Carrier) where
       Binomial.expansion 0            ∎
 
     theorem n+1@(suc n) = begin
-      (x + y) ^ n+1                         ≡⟨⟩
-      (x + y) * (x + y) ^ n                 ≈⟨ *-congˡ (theorem n) ⟩
-      (x + y) * expansion                   ≈⟨ distribʳ _ _ _ ⟩
-      x * expansion + y * expansion         ≈⟨ +-cong lemma₁ lemma₂ ⟩
-      sum₁ + sum₂                           ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
-      ∑[ i < suc n+1 ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n) ⟩
-      ∑[ i < suc n+1 ] Binomial.term n+1 i  ≡⟨⟩
-      Binomial.expansion n+1                ∎
+      (x + y) ^ n+1                     ≡⟨⟩
+      (x + y) * (x + y) ^ n             ≈⟨ *-congˡ (theorem n) ⟩
+      (x + y) * expansion               ≈⟨ distribʳ _ _ _ ⟩
+      x * expansion + y * expansion     ≈⟨ +-cong lemma₁ lemma₂ ⟩
+      sum₁ + sum₂                       ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
+      ∑[ i ≤ n+1 ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n) ⟩
+      ∑[ i ≤ n+1 ] Binomial.term n+1 i  ≡⟨⟩
+      Binomial.expansion n+1            ∎
       where
         open Binomial n
         open BinomialLemmas n

From 854eb384931a3b0a434327d25df8f12ea612c282 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 19 Sep 2023 09:58:04 +0100
Subject: [PATCH 16/19] Update Binomial.agda to bring up to date with #1923

---
 src/Algebra/Properties/Semiring/Binomial.agda | 33 +++++++++----------
 1 file changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 655e864f18..1bda64998a 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -18,12 +18,11 @@ open import Data.Fin.Base as Fin
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties as Fin
   using (toℕ<n; toℕ-fromℕ; toℕ-inject₁)
-open import Data.Fin.Relation.Unary.TopBinomial
-  using (view; top; inj; view-inj; view-top)
+open import Data.Fin.Relation.Unary.Top
+  using (view; ‵fromℕ; ‵inject₁; view-fromℕ; view-inject₁)
 open import Function.Base using (_∘_)
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; cong; module ≡-Reasoning)
-  renaming (refl to ≡-refl)
 
 module Algebra.Properties.Semiring.Binomial {a ℓ} (S : Semiring a ℓ) where
 
@@ -71,8 +70,8 @@ module _ (x y : Carrier) where
 
     term₂ : (i : Fin (suc (suc n))) → Carrier
     term₂ i with view i
-    ... | top   = 0#
-    ... | inj j = y * term j
+    ... | ‵fromℕ     = 0#
+    ... | ‵inject₁ j = y * term j
 
     sum₂ : Carrier
     sum₂ = ∑[ i ≤ suc n ] term₂ i
@@ -105,8 +104,8 @@ module _ (x y : Carrier) where
       ∑[ i ≤ n ] (y * term i)
         ≈˘⟨ +-identityʳ _ ⟩
       ∑[ i ≤ n ] (y * term i) + 0#
-        ≈⟨ +-cong (sum-cong-≋ lemma₂-inj) lemma₂-top ⟩
-      (∑[ i ≤ n ] term₂-inj i) + term₂ [n+1]
+        ≈⟨ +-cong (sum-cong-≋ lemma₂-inject₁) lemma₂-fromℕ ⟩
+      (∑[ i ≤ n ] term₂-inject₁ i) + term₂ [n+1]
         ≈˘⟨ sum-init-last term₂ ⟩
       sum term₂
         ≡⟨⟩
@@ -114,14 +113,14 @@ module _ (x y : Carrier) where
       where
         [n+1] = fromℕ (suc n)
 
-        lemma₂-top : 0# ≈ term₂ [n+1]
-        lemma₂-top rewrite view-top (suc n) = refl
+        lemma₂-fromℕ : 0# ≈ term₂ [n+1]
+        lemma₂-fromℕ rewrite view-fromℕ  (suc n) = refl
 
-        term₂-inj : (i : Fin (suc n)) → Carrier
-        term₂-inj i = term₂ (inject₁ i)
+        term₂-inject₁ : (i : Fin (suc n)) → Carrier
+        term₂-inject₁ i = term₂ (inject₁ i)
 
-        lemma₂-inj : ∀ i → y * term i ≈ term₂-inj i
-        lemma₂-inj i rewrite view-inj i = refl
+        lemma₂-inject₁ : ∀ i → y * term i ≈ term₂-inject₁ i
+        lemma₂-inject₁ i rewrite view-inject₁ i = refl
 
 ------------------------------------------------------------------------
 -- Next, a lemma which is independent of commutativity
@@ -211,7 +210,7 @@ module _ (x y : Carrier) where
       private
 
         n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
-        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡-refl
+        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡.refl
 
 
       term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
@@ -228,7 +227,7 @@ module _ (x y : Carrier) where
         Binomial.term (suc n) 0F     ∎
 
       term₁+term₂≈term (suc i) with view i
-      ... | top
+      ... | ‵fromℕ {n}
       {- remembering that i = fromℕ n, definitionally -}
         rewrite toℕ-fromℕ n
           | nCn≡1 n
@@ -241,7 +240,7 @@ module _ (x y : Carrier) where
         x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
         1 × (x * x ^ n * 1#)         ∎
 
-      ... | inj j
+      ... | ‵inject₁ j
       {- remembering that i = inject₁ j, definitionally -}
           = begin
         (x * term i) + (y * term (suc j))

From e3e4cdf7c8274097bf5176fe3d40e6cb6faebb8c Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Tue, 19 Sep 2023 09:59:06 +0100
Subject: [PATCH 17/19] Delete temporary copy
 src/Data/Fin/Relation/Unary/TopBinomial.agda

---
 src/Data/Fin/Relation/Unary/TopBinomial.agda | 140 -------------------
 1 file changed, 140 deletions(-)
 delete mode 100644 src/Data/Fin/Relation/Unary/TopBinomial.agda

diff --git a/src/Data/Fin/Relation/Unary/TopBinomial.agda b/src/Data/Fin/Relation/Unary/TopBinomial.agda
deleted file mode 100644
index 68bf9f9fdf..0000000000
--- a/src/Data/Fin/Relation/Unary/TopBinomial.agda
+++ /dev/null
@@ -1,140 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- The 'top' view of Fin
---
--- This is an example of a view of (elements of) a datatype,
--- here i : Fin (suc n), which exhibits every such i as
--- * either, i = fromℕ n
--- * or, i = inject₁ j for a unique j : Fin n
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Data.Fin.Relation.Unary.TopBinomial where
-
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_)
-open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc)
-open import Data.Product using (uncurry)
-open import Data.Fin.Base hiding (_<_)
-open import Data.Fin.Properties as Fin
-  using (suc-injective; toℕ-fromℕ; toℕ<n; toℕ-inject₁; inject₁ℕ<)
-open import Relation.Binary.PropositionalEquality
-
-private
-  variable
-    n : ℕ
-
-------------------------------------------------------------------------
--- The View, considered as a unary relation on Fin (suc n)
-
--- First, a lemma not in `Data.Fin.Properties`,
--- but which establishes disjointness of the
--- (interpretations of the) constructors of the View
-
-top≢inject₁ : ∀ (j : Fin n) → fromℕ n ≢ inject₁ j
-top≢inject₁ (suc j) eq = top≢inject₁ j (suc-injective eq)
-
--- The View, itself
-
-data View : (i : Fin (suc n)) → Set where
-
-  top :                View (fromℕ n)
-  inj : (j : Fin n) → View (inject₁ j)
-
--- The view covering function, witnessing soundness of the view
-
-view : ∀ {n} i → View {n} i
-view {n = zero}  zero = top
-view {n = suc _} zero = inj _
-view {n = suc n} (suc i) with view {n} i
-... | top   = top
-... | inj j = inj (suc j)
-
--- Interpretation of the view constructors
-
-⟦_⟧ : ∀ {i} → View {n} i → Fin (suc n)
-⟦ top ⟧   = fromℕ _
-⟦ inj j ⟧ = inject₁ j
-
--- Completeness of the view
-
-view-complete : ∀ {i} (v : View {n} i) → ⟦ v ⟧ ≡ i
-view-complete top     = refl
-view-complete (inj j) = refl
-
--- 'Computational' behaviour of the covering function
-
-view-top : ∀ n → view {n} (fromℕ n) ≡ top
-view-top zero    = refl
-view-top (suc n) rewrite view-top n = refl
-
-view-inj : ∀ j → view {n} (inject₁ j) ≡ inj j
-view-inj zero       = refl
-view-inj (suc j) rewrite view-inj j = refl
-
-------------------------------------------------------------------------
--- Experimental
---
--- Because we work without K, Agda's unifier will complain about
--- attempts to match `refl` against hypotheses of the form
---    `view {n] i ≡ v`
--- or gets stuck trying to solve unification problems of the form
---    (inferred index ≟ expected index)
--- even when these problems are *provably* solvable.
---
--- So the two predicates on values of the view defined below
--- are extensionally equivalent to the assertions
--- `view {n] i ≡ top` and `view {n] i ≡ inj j`
---
--- But such assertions can only ever have a unique (irrelevant) proof
--- so we introduce instances to witness them, themselves given by
--- the functions `view-top` and `view-inj` defined above
-
-module Instances {n} where
-
-  data IsTop : ∀ {i} → View {n} i → Set where
-
-    top : IsTop top
-
-  instance
-
-    top⁺ : IsTop {i = fromℕ n} (view (fromℕ n))
-    top⁺ rewrite view-top n = top
-
-  data IsInj : ∀ {i} → View {n} i → Set where
-
-    inj : ∀ j → IsInj (inj j)
-
-  instance
-
-    inj⁺ : ∀ {j} → IsInj (view (inject₁ j))
-    inj⁺ {j} rewrite view-inj j = inj j
-
-    inject₁≡⁺ : ∀ {i} {j} {eq : inject₁ i ≡ j} → IsInj (view j)
-    inject₁≡⁺ {eq = refl} = inj⁺
-
-    n≢inject₁⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view i)
-    n≢inject₁⁺ {i} {n≢i} with view i
-    ... | top   = ⊥-elim (n≢i (begin
-      n                         ≡˘⟨ toℕ-fromℕ n ⟩
-      toℕ (fromℕ n)           ≡˘⟨ toℕ-inject₁ (fromℕ n) ⟩
-      toℕ (inject₁ (fromℕ n)) ∎)) where open ≡-Reasoning
-    ... | inj j = inj j
-
-open Instances
-
-------------------------------------------------------------------------
--- As a corollary, we obtain two useful properties, which are
--- witnessed by, but can also serve as proxy replacements for,
--- the corresponding properties in `Data.Fin.Properties`
-
-module _ {n} where
-
-  view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n
-  view-top-toℕ i with top ← view i = toℕ-fromℕ n
-
-  view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n
-  view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j
-

From 3b67531aaff16ae039c7cb80bda34eeb71ca87a6 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 28 Sep 2023 09:15:43 +0900
Subject: [PATCH 18/19] Flattened module structure

---
 .../CommutativeSemiring/Binomial.agda         |   2 +-
 src/Algebra/Properties/Semiring/Binomial.agda | 412 ++++++++----------
 2 files changed, 175 insertions(+), 239 deletions(-)

diff --git a/src/Algebra/Properties/CommutativeSemiring/Binomial.agda b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
index 688dc8978f..7a5524f3e8 100644
--- a/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
+++ b/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
@@ -19,6 +19,6 @@ open Binomial public hiding (theorem)
 ------------------------------------------------------------------------
 -- Here it is
 
-theorem : ∀ n x y → ((x + y) ^ n) ≈ Binomial.expansion x y n
+theorem : ∀ n x y → (x + y) ^ n ≈ binomialExpansion x y n
 theorem n x y = Binomial.theorem x y (*-comm x y) n
 
diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 1bda64998a..9eb2d6fc6a 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -2,6 +2,8 @@
 -- The Agda standard library
 --
 -- The Binomial Theorem for *-commuting elements in a Semiring
+--
+-- Freely adapted from PR #1287 by Maciej Piechotka (@uzytkownik)
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -22,278 +24,212 @@ open import Data.Fin.Relation.Unary.Top
   using (view; ‵fromℕ; ‵inject₁; view-fromℕ; view-inject₁)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; cong; module ≡-Reasoning)
+  using (_≡_; _≢_; cong)
 
-module Algebra.Properties.Semiring.Binomial {a ℓ} (S : Semiring a ℓ) where
+module Algebra.Properties.Semiring.Binomial
+  {a ℓ} (S : Semiring a ℓ)
+  (open Semiring S)
+  (x y : Carrier)
+  where
 
-open Semiring S
 open import Algebra.Definitions _≈_
-open import Algebra.Structures _≈_
 open import Algebra.Properties.Semiring.Sum S
 open import Algebra.Properties.Semiring.Mult S
 open import Algebra.Properties.Semiring.Exp S
-import Relation.Binary.Reasoning.Setoid setoid as ≈-Reasoning
-
-
-------------------------------------------------------------------------
--- The Binomial Theorem for *-commuting elements in a Semiring
--- Freely adapted from PR #1287 by Maciej Piechotka (@uzytkownik)
-
-module _ (x y : Carrier) where
+open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
 -- Definitions
 
-  module Binomial (n : ℕ) where
-
-    module _ (i : Fin (suc n)) where
+-- Note - `n` could be explicit in many of these definitions, but the
+-- code is more readable if left explicit.
 
-      private
-        k   = toℕ i
-        n-k = n ∸ k
+binomial : (n : ℕ) → Fin (suc n) → Carrier
+binomial n k = (x ^ toℕ k) * (y ^ (n ∸ toℕ k))
 
-      binomial : Carrier
-      binomial = (x ^ k) * (y ^ n-k)
+binomialTerm : (n : ℕ) → Fin (suc n) → Carrier
+binomialTerm n k = (n C toℕ k) × binomial n k
 
-      term : Carrier
-      term = (n C k) × binomial
+binomialExpansion : ℕ → Carrier
+binomialExpansion n = ∑[ k ≤ n ] (binomialTerm n k)
 
-    expansion : Carrier
-    expansion = ∑[ i ≤ n ] term i
+term₁ : (n : ℕ) → Fin (suc (suc n)) → Carrier
+term₁ n zero    = 0#
+term₁ n (suc k) = x * (binomialTerm n k)
 
-    term₁ : (i : Fin (suc (suc n))) → Carrier
-    term₁ zero    = 0#
-    term₁ (suc i) = x * term i
+term₂ : (n : ℕ) → Fin (suc (suc n)) → Carrier
+term₂ n k with view k
+... | ‵fromℕ     = 0#
+... | ‵inject₁ j = y * binomialTerm n j
 
-    sum₁ : Carrier
-    sum₁ = ∑[ i ≤ suc n ] term₁ i
+sum₁ : ℕ → Carrier
+sum₁ n = ∑[ k ≤ suc n ] term₁ n k
 
-    term₂ : (i : Fin (suc (suc n))) → Carrier
-    term₂ i with view i
-    ... | ‵fromℕ     = 0#
-    ... | ‵inject₁ j = y * term j
-
-    sum₂ : Carrier
-    sum₂ = ∑[ i ≤ suc n ] term₂ i
+sum₂ : ℕ → Carrier
+sum₂ n = ∑[ k ≤ suc n ] term₂ n k
 
 ------------------------------------------------------------------------
 -- Properties
 
-  module BinomialLemmas (n : ℕ) where
-
-    open Binomial n
-
-    open ≈-Reasoning
-
-    lemma₁ : x * expansion ≈ sum₁
-    lemma₁ = begin
-      x * expansion
-        ≈⟨ *-distribˡ-sum x term ⟩
-      ∑[ i ≤ n ] (x * term i)
-        ≈˘⟨ +-identityˡ _ ⟩
-      (0# + ∑[ i ≤ n ] (x * term i))
-        ≡⟨⟩
-      (0# + ∑[ i ≤ n ] term₁ (suc i))
-        ≡⟨⟩
-      sum₁  ∎
-
-    lemma₂ : y * expansion ≈ sum₂
-    lemma₂ = begin
-      (y * expansion)
-        ≈⟨ *-distribˡ-sum y term ⟩
-      ∑[ i ≤ n ] (y * term i)
-        ≈˘⟨ +-identityʳ _ ⟩
-      ∑[ i ≤ n ] (y * term i) + 0#
-        ≈⟨ +-cong (sum-cong-≋ lemma₂-inject₁) lemma₂-fromℕ ⟩
-      (∑[ i ≤ n ] term₂-inject₁ i) + term₂ [n+1]
-        ≈˘⟨ sum-init-last term₂ ⟩
-      sum term₂
-        ≡⟨⟩
-      sum₂  ∎
-      where
-        [n+1] = fromℕ (suc n)
-
-        lemma₂-fromℕ : 0# ≈ term₂ [n+1]
-        lemma₂-fromℕ rewrite view-fromℕ  (suc n) = refl
-
-        term₂-inject₁ : (i : Fin (suc n)) → Carrier
-        term₂-inject₁ i = term₂ (inject₁ i)
-
-        lemma₂-inject₁ : ∀ i → y * term i ≈ term₂-inject₁ i
-        lemma₂-inject₁ i rewrite view-inject₁ i = refl
+term₂[n,n+1]≈0# : ∀ n → term₂ n (fromℕ (suc n)) ≈ 0# 
+term₂[n,n+1]≈0# n rewrite view-fromℕ (suc n) = refl
+
+lemma₁ : ∀ n → x * binomialExpansion n ≈ sum₁ n
+lemma₁ n = begin
+  x * binomialExpansion n                ≈⟨ *-distribˡ-sum x (binomialTerm n) ⟩
+  ∑[ i ≤ n ] (x * binomialTerm n i)      ≈˘⟨ +-identityˡ _ ⟩
+  0# + ∑[ i ≤ n ] (x * binomialTerm n i) ≡⟨⟩
+  0# + ∑[ i ≤ n ] term₁ n (suc i)        ≡⟨⟩
+  sum₁ n                                 ∎
+
+lemma₂ : ∀ n → y * binomialExpansion n ≈ sum₂ n
+lemma₂ n = begin
+  y * binomialExpansion n                       ≈⟨ *-distribˡ-sum y (binomialTerm n) ⟩
+  ∑[ i ≤ n ] (y * binomialTerm n i)             ≈˘⟨ +-identityʳ _ ⟩
+  ∑[ i ≤ n ] (y * binomialTerm n i) + 0#        ≈⟨ +-cong (sum-cong-≋ lemma₂-inject₁) (sym (term₂[n,n+1]≈0# n)) ⟩
+  (∑[ i ≤ n ] term₂-inject₁ i) + term₂ n [n+1]  ≈˘⟨ sum-init-last (term₂ n) ⟩
+  sum (term₂ n)                                 ≡⟨⟩
+  sum₂ n                                        ∎
+  where
+    [n+1] = fromℕ (suc n)
+
+    term₂-inject₁ : (i : Fin (suc n)) → Carrier
+    term₂-inject₁ i = term₂ n (inject₁ i)
+
+    lemma₂-inject₁ : ∀ i → y * binomialTerm n i ≈ term₂-inject₁ i
+    lemma₂-inject₁ i rewrite view-inject₁ i = refl
 
 ------------------------------------------------------------------------
 -- Next, a lemma which is independent of commutativity
 
-  module _ {n} (i : Fin (suc n)) where
-
-    open Binomial n using (term)
-
-    private
-
-      k = toℕ i
-
-    x*lemma : x * term i ≈ (n C k) × Binomial.binomial (suc n) (suc i)
-    x*lemma = begin
-      x * term i                                  ≡⟨⟩
-      x * ((n C k) × (x ^ k * y ^ (n ∸ k)))       ≈˘⟨ *-congˡ (×-assoc-* (n C k) _ _) ⟩
-      x * ((n C k) × x ^ k * y ^ (n ∸ k))         ≈˘⟨ *-assoc x ((n C k) × x ^ k) _ ⟩
-      (x * (n C k) × x ^ k) * y ^ (n ∸ k)         ≈⟨ *-congʳ (×-comm-* (n C k) _ _) ⟩
-      (n C k) × x ^ (suc k) * y ^ (n ∸ k)         ≡⟨⟩
-      (n C k) × x ^ (suc k) * y ^ (suc n ∸ suc k) ≈⟨ ×-assoc-* (n C k) _ _ ⟩
-      (n C k) × Binomial.binomial (suc n) (suc i) ∎
-      where
-        open ≈-Reasoning
-
-
+x*lemma : ∀ {n} (i : Fin (suc n)) →
+          x * binomialTerm n i ≈ (n C toℕ i) × binomial (suc n) (suc i)
+x*lemma {n} i = begin
+  x * binomialTerm n i                        ≡⟨⟩
+  x * ((n C k) × (x ^ k * y ^ (n ∸ k)))       ≈˘⟨ *-congˡ (×-assoc-* (n C k) _ _) ⟩
+  x * ((n C k) × x ^ k * y ^ (n ∸ k))         ≈˘⟨ *-assoc x ((n C k) × x ^ k) _ ⟩
+  (x * (n C k) × x ^ k) * y ^ (n ∸ k)         ≈⟨ *-congʳ (×-comm-* (n C k) _ _) ⟩
+  (n C k) × x ^ (suc k) * y ^ (n ∸ k)         ≡⟨⟩
+  (n C k) × x ^ (suc k) * y ^ (suc n ∸ suc k) ≈⟨ ×-assoc-* (n C k) _ _ ⟩
+  (n C k) × binomial (suc n) (suc i)          ∎
+  where k = toℕ i
 
 ------------------------------------------------------------------------
 -- Next, a lemma which does require commutativity
 
-  module _ (x*y≈y*x : x * y ≈ y * x) where
-
-    module _ {n : ℕ} (j : Fin n) where
-
-      open Binomial n using (binomial; term)
-
-      private
-
-        i = inject₁ j
-
-      y*lemma : y * term (suc j) ≈ (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i)
-      y*lemma = begin
-        y * term (suc j)
-          ≈⟨ ×-comm-* nC[j+1] y (binomial (suc j)) ⟩
-        nC[j+1] × (y * binomial (suc j))
-          ≈⟨ ×-congʳ nC[j+1] (y*x^m*y^n≈x^m*y^[n+1] x*y≈y*x [j+1] [n-j-1]) ⟩
-        nC[j+1] × (x ^ [j+1] * y ^ [n-j])
-          ≈˘⟨ ×-congʳ nC[j+1] (*-congʳ (^-congʳ x [k+1]≡[j+1])) ⟩
-        nC[j+1] × (x ^ [k+1] * y ^ [n-j])
-          ≈˘⟨ ×-congʳ nC[j+1] (*-congˡ (^-congʳ y [n-k]≡[n-j])) ⟩
-        nC[j+1] × (x ^ [k+1] * y ^ [n-k])
-          ≡⟨⟩
-        nC[j+1] × (x ^ [k+1] * y ^ [n+1]-[k+1])
-          ≡⟨⟩
-        (n C toℕ (suc j)) × Binomial.binomial (suc n) (suc i) ∎
-        where
-          k           = toℕ i
-          k≡j         : k ≡ toℕ j
-          k≡j         = toℕ-inject₁ j
-
-          [k+1]       = ℕ.suc k
-          [j+1]       = toℕ (suc j)
-          [n-k]       = n ∸ k
-          [n+1]-[k+1] = [n-k]
-          [n-j-1]     = n ∸ [j+1]
-          [n-j]       = ℕ.suc [n-j-1]
-          nC[j+1]     = n C [j+1]
-
-          [k+1]≡[j+1] : [k+1] ≡ [j+1]
-          [k+1]≡[j+1] = cong suc k≡j
-
-          [n-k]≡[n-j] : [n-k] ≡ [n-j]
-          [n-k]≡[n-j] = begin
-            [n-k]      ≡⟨ cong (n ∸_) k≡j ⟩
-            n ∸ toℕ j  ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟩
-            [n-j]      ∎ where open ≡-Reasoning
-          open ≈-Reasoning
+y*lemma : x * y ≈ y * x → ∀ {n : ℕ} (j : Fin n) → 
+          y * binomialTerm n (suc j) ≈ (n C toℕ (suc j)) × binomial (suc n) (suc (inject₁ j))
+y*lemma x*y≈y*x {n} j = begin
+  y * binomialTerm n (suc j)
+    ≈⟨ ×-comm-* nC[j+1] y (binomial n (suc j)) ⟩
+  nC[j+1] × (y * binomial n (suc j))
+    ≈⟨ ×-congʳ nC[j+1] (y*x^m*y^n≈x^m*y^[n+1] x*y≈y*x [j+1] [n-j-1]) ⟩
+  nC[j+1] × (x ^ [j+1] * y ^ [n-j])
+    ≈˘⟨ ×-congʳ nC[j+1] (*-congʳ (^-congʳ x (cong suc k≡j))) ⟩
+  nC[j+1] × (x ^ [k+1] * y ^ [n-j])
+    ≈˘⟨ ×-congʳ nC[j+1] (*-congˡ (^-congʳ y [n-k]≡[n-j])) ⟩
+  nC[j+1] × (x ^ [k+1] * y ^ [n-k])
+    ≡⟨⟩
+  nC[j+1] × (x ^ [k+1] * y ^ [n+1]-[k+1])
+    ≡⟨⟩
+  (n C toℕ (suc j)) × binomial (suc n) (suc i) ∎
+  where
+    i           = inject₁ j
+    k           = toℕ i
+    [k+1]       = ℕ.suc k
+    [j+1]       = toℕ (suc j)
+    [n-k]       = n ∸ k
+    [n+1]-[k+1] = [n-k]
+    [n-j-1]     = n ∸ [j+1]
+    [n-j]       = ℕ.suc [n-j-1]
+    nC[j+1]     = n C [j+1]
+
+    k≡j         : k ≡ toℕ j
+    k≡j         = toℕ-inject₁ j
+
+    [n-k]≡[n-j] : [n-k] ≡ [n-j]
+    [n-k]≡[n-j] = ≡.trans (cong (n ∸_) k≡j) (+-∸-assoc 1 (toℕ<n j))
 
 ------------------------------------------------------------------------
 -- Now, a lemma characterising the sum of the term₁ and term₂ expressions
 
-    module _ n where
-
-      open ≈-Reasoning
-
-      open Binomial n using (term; term₁; term₂)
-
-      private
-
-        n<ᵇ1+n : (n Nat.<ᵇ suc n) ≡ true
-        n<ᵇ1+n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡.refl
-
-
-      term₁+term₂≈term : ∀ i → term₁ i + term₂ i ≈ Binomial.term (suc n) i
-
-      term₁+term₂≈term 0F = begin
-        term₁ 0F + term₂ 0F          ≡⟨⟩
-        0# + y * (1 × (1# * y ^ n))  ≈⟨ +-identityˡ _ ⟩
-        y * (1 × (1# * y ^ n))       ≈⟨ *-congˡ (+-identityʳ (1# * y ^ n)) ⟩
-        y * (1# * y ^ n)             ≈⟨ *-congˡ (*-identityˡ (y ^ n)) ⟩
-        y * y ^ n                    ≡⟨⟩
-        y ^ suc n                    ≈˘⟨ *-identityˡ (y ^ suc n) ⟩
-        1# * y ^ suc n               ≈˘⟨ +-identityʳ (1# * y ^ suc n) ⟩
-        1 × (1# * y ^ suc n)         ≡⟨⟩
-        Binomial.term (suc n) 0F     ∎
-
-      term₁+term₂≈term (suc i) with view i
-      ... | ‵fromℕ {n}
-      {- remembering that i = fromℕ n, definitionally -}
-        rewrite toℕ-fromℕ n
-          | nCn≡1 n
-          | n∸n≡0 n
-          | n<ᵇ1+n
-          = begin
-        x * ((x ^ n * 1#) + 0#) + 0# ≈⟨ +-identityʳ _ ⟩
-        x * ((x ^ n * 1#) + 0#)      ≈⟨ *-congˡ (+-identityʳ _) ⟩
-        x * (x ^ n * 1#)             ≈˘⟨ *-assoc _ _ _ ⟩
-        x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
-        1 × (x * x ^ n * 1#)         ∎
-
-      ... | ‵inject₁ j
-      {- remembering that i = inject₁ j, definitionally -}
-          = begin
-        (x * term i) + (y * term (suc j))
-          ≈⟨ +-cong (x*lemma i) (y*lemma j) ⟩
-        (nCk × [x^k+1]*[y^n-k]) + (nC[j+1] × [x^k+1]*[y^n-k])
-          ≈˘⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟩
-        (nCk × [x^k+1]*[y^n-k]) + (nC[k+1] × [x^k+1]*[y^n-k])
-          ≈˘⟨ ×-homo-+ [x^k+1]*[y^n-k] nCk nC[k+1] ⟩
-        (nCk Nat.+ nC[k+1]) × [x^k+1]*[y^n-k]
-          ≡⟨ cong (_× [x^k+1]*[y^n-k]) (nCk+nC[k+1]≡[n+1]C[k+1] n k) ⟩
-        ((suc n) C (suc k)) × [x^k+1]*[y^n-k]
-          ≡⟨⟩
-        Binomial.term (suc n) (suc i) ∎
-          where
-            k               = toℕ i
-            [k+1]           = ℕ.suc k
-            [j+1]           = toℕ (suc j)
-            nCk             = n C k
-            nC[k+1]         = n C [k+1]
-            nC[j+1]         = n C [j+1]
-            nC[k+1]≡nC[j+1] : nC[k+1] ≡ nC[j+1]
-            nC[k+1]≡nC[j+1] = cong ((n C_) ∘ suc) (toℕ-inject₁ j)
-            [x^k+1]*[y^n-k] : Carrier
-            [x^k+1]*[y^n-k] = Binomial.binomial (suc n) (suc i)
+private
+  n<ᵇ1+n : ∀ n → (n Nat.<ᵇ suc n) ≡ true
+  n<ᵇ1+n n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡.refl
+
+term₁+term₂≈term : x * y ≈ y * x → ∀ n i → term₁ n i + term₂ n i ≈ binomialTerm (suc n) i
+
+term₁+term₂≈term x*y≈y*x n 0F = begin
+  term₁ n 0F + term₂ n 0F      ≡⟨⟩
+  0# + y * (1 × (1# * y ^ n))  ≈⟨ +-identityˡ _ ⟩
+  y * (1 × (1# * y ^ n))       ≈⟨ *-congˡ (+-identityʳ (1# * y ^ n)) ⟩
+  y * (1# * y ^ n)             ≈⟨ *-congˡ (*-identityˡ (y ^ n)) ⟩
+  y * y ^ n                    ≡⟨⟩
+  y ^ suc n                    ≈˘⟨ *-identityˡ (y ^ suc n) ⟩
+  1# * y ^ suc n               ≈˘⟨ +-identityʳ (1# * y ^ suc n) ⟩
+  1 × (1# * y ^ suc n)         ≡⟨⟩
+  binomialTerm (suc n) 0F      ∎
+
+term₁+term₂≈term x*y≈y*x n (suc i) with view i
+... | ‵fromℕ {n}
+{- remembering that i = fromℕ n, definitionally -}
+  rewrite toℕ-fromℕ n
+    | nCn≡1 n
+    | n∸n≡0 n
+    | n<ᵇ1+n n
+    = begin
+  x * ((x ^ n * 1#) + 0#) + 0# ≈⟨ +-identityʳ _ ⟩
+  x * ((x ^ n * 1#) + 0#)      ≈⟨ *-congˡ (+-identityʳ _) ⟩
+  x * (x ^ n * 1#)             ≈˘⟨ *-assoc _ _ _ ⟩
+  x * x ^ n * 1#               ≈˘⟨ +-identityʳ _ ⟩
+  1 × (x * x ^ n * 1#)         ∎
+
+... | ‵inject₁ j
+{- remembering that i = inject₁ j, definitionally -}
+    = begin
+  (x * binomialTerm n i) + (y * binomialTerm n (suc j))
+    ≈⟨ +-cong (x*lemma i) (y*lemma x*y≈y*x j) ⟩
+  (nCk × [x^k+1]*[y^n-k]) + (nC[j+1] × [x^k+1]*[y^n-k])
+    ≈˘⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟩
+  (nCk × [x^k+1]*[y^n-k]) + (nC[k+1] × [x^k+1]*[y^n-k])
+    ≈˘⟨ ×-homo-+ [x^k+1]*[y^n-k] nCk nC[k+1] ⟩
+  (nCk Nat.+ nC[k+1]) × [x^k+1]*[y^n-k]
+    ≡⟨ cong (_× [x^k+1]*[y^n-k]) (nCk+nC[k+1]≡[n+1]C[k+1] n k) ⟩
+  ((suc n) C (suc k)) × [x^k+1]*[y^n-k]
+    ≡⟨⟩
+  binomialTerm (suc n) (suc i) ∎
+  where
+    k               = toℕ i
+    [k+1]           = ℕ.suc k
+    [j+1]           = toℕ (suc j)
+    nCk             = n C k
+    nC[k+1]         = n C [k+1]
+    nC[j+1]         = n C [j+1]
+    [x^k+1]*[y^n-k] = binomial (suc n) (suc i)
+
+    nC[k+1]≡nC[j+1] : nC[k+1] ≡ nC[j+1]
+    nC[k+1]≡nC[j+1] = cong ((n C_) ∘ suc) (toℕ-inject₁ j)
 
 ------------------------------------------------------------------------
 -- Finally, the main result
 
-    open ≈-Reasoning
-
-    theorem : ∀ n → ((x + y) ^ n) ≈ Binomial.expansion n
-
-    theorem zero    = begin
-      (x + y) ^ 0                     ≡⟨⟩
-      1#                              ≈˘⟨ 1×-identityʳ 1# ⟩
-      1 × 1#                          ≈˘⟨ *-identityʳ (1 × 1#) ⟩
-      (1 × 1#) * 1#                   ≈⟨ ×-assoc-* 1 1# 1# ⟩
-      1 × (1# * 1#)                   ≡⟨⟩
-      1 × (x ^ 0 * y ^ 0)             ≈˘⟨ +-identityʳ _ ⟩
-      1 × (x ^ 0 * y ^ 0) + 0#        ≡⟨⟩
-      (0 C 0) × (x ^ 0 * y ^ 0) + 0#  ≡⟨⟩
-      Binomial.expansion 0            ∎
-
-    theorem n+1@(suc n) = begin
-      (x + y) ^ n+1                     ≡⟨⟩
-      (x + y) * (x + y) ^ n             ≈⟨ *-congˡ (theorem n) ⟩
-      (x + y) * expansion               ≈⟨ distribʳ _ _ _ ⟩
-      x * expansion + y * expansion     ≈⟨ +-cong lemma₁ lemma₂ ⟩
-      sum₁ + sum₂                       ≈˘⟨ ∑-distrib-+ term₁ term₂ ⟩
-      ∑[ i ≤ n+1 ] (term₁ i + term₂ i)  ≈⟨ sum-cong-≋ (term₁+term₂≈term n) ⟩
-      ∑[ i ≤ n+1 ] Binomial.term n+1 i  ≡⟨⟩
-      Binomial.expansion n+1            ∎
-      where
-        open Binomial n
-        open BinomialLemmas n
-
+theorem : x * y ≈ y * x → ∀ n → (x + y) ^ n ≈ binomialExpansion n
+theorem x*y≈y*x zero    = begin
+  (x + y) ^ 0                     ≡⟨⟩
+  1#                              ≈˘⟨ 1×-identityʳ 1# ⟩
+  1 × 1#                          ≈˘⟨ *-identityʳ (1 × 1#) ⟩
+  (1 × 1#) * 1#                   ≈⟨ ×-assoc-* 1 1# 1# ⟩
+  1 × (1# * 1#)                   ≡⟨⟩
+  1 × (x ^ 0 * y ^ 0)             ≈˘⟨ +-identityʳ _ ⟩
+  1 × (x ^ 0 * y ^ 0) + 0#        ≡⟨⟩
+  (0 C 0) × (x ^ 0 * y ^ 0) + 0#  ≡⟨⟩
+  binomialExpansion 0             ∎
+theorem x*y≈y*x n+1@(suc n) = begin
+  (x + y) ^ n+1                                     ≡⟨⟩
+  (x + y) * (x + y) ^ n                             ≈⟨ *-congˡ (theorem x*y≈y*x n) ⟩
+  (x + y) * binomialExpansion n                     ≈⟨ distribʳ _ _ _ ⟩
+  x * binomialExpansion n + y * binomialExpansion n ≈⟨ +-cong (lemma₁ n) (lemma₂ n) ⟩
+  sum₁ n + sum₂ n                                   ≈˘⟨ ∑-distrib-+ (term₁ n) (term₂ n) ⟩
+  ∑[ i ≤ n+1 ] (term₁ n i + term₂ n i)              ≈⟨ sum-cong-≋ (term₁+term₂≈term x*y≈y*x n) ⟩
+  ∑[ i ≤ n+1 ] binomialTerm n+1 i                   ≡⟨⟩
+  binomialExpansion n+1                             ∎

From 11e2fb3cd5383f548f233bbafd41e8c3a6f01e97 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Thu, 28 Sep 2023 15:50:15 +0900
Subject: [PATCH 19/19] Fix comment

---
 src/Algebra/Properties/Semiring/Binomial.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Algebra/Properties/Semiring/Binomial.agda b/src/Algebra/Properties/Semiring/Binomial.agda
index 9eb2d6fc6a..b4d5ef81db 100644
--- a/src/Algebra/Properties/Semiring/Binomial.agda
+++ b/src/Algebra/Properties/Semiring/Binomial.agda
@@ -41,7 +41,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 ------------------------------------------------------------------------
 -- Definitions
 
--- Note - `n` could be explicit in many of these definitions, but the
+-- Note - `n` could be implicit in many of these definitions, but the
 -- code is more readable if left explicit.
 
 binomial : (n : ℕ) → Fin (suc n) → Carrier
@@ -144,8 +144,8 @@ y*lemma x*y≈y*x {n} j = begin
     [n-j]       = ℕ.suc [n-j-1]
     nC[j+1]     = n C [j+1]
 
-    k≡j         : k ≡ toℕ j
-    k≡j         = toℕ-inject₁ j
+    k≡j : k ≡ toℕ j
+    k≡j = toℕ-inject₁ j
 
     [n-k]≡[n-j] : [n-k] ≡ [n-j]
     [n-k]≡[n-j] = ≡.trans (cong (n ∸_) k≡j) (+-∸-assoc 1 (toℕ<n j))