    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The Binomial Theorem for Commutative Semirings
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --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 ≈ binomialExpansion x y n
    theorem n x y = Binomial.theorem x y (*-comm x y) n