module My.SetTheory.Nat.IdentityElement where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Algebra.Structures as AS
import Data.Nat as DN
import Data.Nat.Properties as DNP
import Data.Product as DP
import Function as F
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_*_)
open F using (_$_)
open RBPE using (_≡_)

-- §──────────────────────────────────────────────────────────────────
-- Identity element
-- §──────────────────────────────────────────────────────────────────

1*n≡n : (n : DN.ℕ) →  * n ≡ n
1*n≡n = DP.proj₁ CSR.*-identity
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring

1*n≡n' : (n : DN.ℕ) →  * n ≡ n
1*n≡n' = DP.proj₁ $ A.CommutativeSemiring.*-identity DNP.commutativeSemiring

n*1≡n : (n : DN.ℕ) → n *  ≡ n
n*1≡n = DP.proj₂ CSR.*-identity
  where
    module CSR = A.CommutativeSemiring DNP.commutativeSemiring