SemigroupRing.tex

\chapter{Theory Of Semigroup And Ring In Agda}
In early 20th century, mathematician Hilbert proposed the H\textsubscript{10}
problem: "Is there a general approach to verify whether a Diophantine equation
is solvable ?" \cite{larchey2020hilbert}. Although this problem was solved by
1970, in 1987 Siekmann and Szabo concluded that the unification problem of
D\textsubscript{A}-rewriting system\cite{DARewriting} cannot be predicted. In
\cite{deng2016characterizations}, the author uses a \textit{semigroup} to give a
general construct of D\textsubscript{A}-rewriting system. Semigroup structures
are also used in finite automata systems, probability theory and partial
differential equations \cite{liaqat2021some}.

Similarly, \textit{ring} is an algebraic structure that also has notable
applications in number theory \cite{pedrouzo2021revisiting}, in quantum
computing \cite{netto2008influence}, in cryptography
\cite{khathuria2021algebraic}, and many other fields. Variations of ring
structure such as near-ring, quasi-ring, and non-associative rings are explored
to make ring theory (study of ring structures), more dynamic, concrete and
useable. Now, the question arises: how can we encode these structures in Agda?
We will explore this question in this chapter. This chapter aims to define these
structures and prove some properties in the Agda standard library that can help
build other systems that use these structures. 

\section{Definition}
A semigroup is an algebraic structure that consists of a set equipped with an
associative binary operation. Formally, a semigroup is defined as: Let $S$ be a
set, and let $∙$ be a binary operation on S, the structure $(S,∙)$ is a
semigroup if the following property holds:
\[\forall\ x\ y\ z\ \in\ S ,\ x\ ∙\ (y\ ∙\ z)\ =\ (x\ ∙\ y)\ ∙\ z\]

A semigroup that satisfies the commutative property is called a commutative
semigroup. For binary operation \( ∙ \) on a set S, commutative property is
defined as:
\[ \forall\ x\ y\ \in\ S ,\ x\ ∙\ y\ =\ y\ ∙\ x\ \]

In Agda, the above predicates can be written as:

\begin{minted}[breaklines,samepage]{Agda}
Associative : Op₂ A → Set _
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

Commutative : Op₂ A → Set _
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
\end{minted}

In Agda, we can define a semigroup as a record type to ensure that the
properties of the semigroup are satisfied.

\begin{minted}[breaklines,samepage]{Agda}
record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
field
  isMagma : IsMagma ∙
  assoc   : Associative ∙

open IsMagma isMagma public
\end{minted}

Similarly, commutative semigroup can be defined using semigroup as: 

\begin{minted}[breaklines,samepage]{Agda}
record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
field
  isSemigroup : IsSemigroup ∙
  comm        : Commutative ∙

open IsSemigroup isSemigroup public
\end{minted}

We may encode various ring structures as follows: Non-associative ring on set
$R$ is an algebraic structure with two binary operations $(+)$ addition and
$(*)$ multiplication. Addition $(R,+,⁻¹,0)$ is an Abelian group that is a group
with commutative property. Multiplication $(R,*,1)$ is a unital magma that is a
magma with identity. A group is a monoid with an inverse and a monoid is a
semigroup with identity. A magma is called unital if it has an identity. In a
non-associative ring, multiplication distributes over addition, and it has an
annihilating zero. Formally, nonAssociativeRing $(R,+,*,^{-1},0,1)$ should
satisfy the following identities:
\begin{itemize}
  \item $(R,+,⁻¹,0)$ is an Abelian Group:
   \begin{itemize}
    \item Associativity: $\forall x,y,z \in R, x + (y + z) = (x + y) + z$
    \item commutativity : $\forall x,y \in R, (x + y) = (y + x)$
    \item Identity: $\forall x \in R, (x + 0) = x = (0 + x)$
    \item Inverse: $\forall x \in R, (x + x⁻¹) = 0 = (x⁻¹ + x)$
  \end{itemize}
  \item $(R,*,1)$ is a unital magma
  \begin{itemize}
    \item Identity: $\forall x,y \in R, (x * 1) = x = (1 * x)$
  \end{itemize}
  \item Multiplication distributes over addition: \(\forall x , y , z \in R, (x
  * (y + z)) = (x * y) + (x * z)\) and \( (x + y) * z = (x * z) + (y * z) \)
  \item Annihilating zero: \(\forall x \in R, (x * 0) = 0 = (0 * x)\)
\end{itemize}

\begin{minted}[breaklines,samepage]{Agda}
record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
 field
   +-isAbelianGroup : IsAbelianGroup + 0# -_
   *-cong           : Congruent₂ *
   *-identity       : Identity 1# *
   distrib          : * DistributesOver +
   zero             : Zero 0# *

 open IsAbelianGroup +-isAbelianGroup public
\end{minted}

We don't define \inline{IsNonAssociativeRing} with \inline{*-isUnitalMagma} to
remove the redundant equivalence relation. This is discussed in Chapter 8. The
same technique is followed when defining other ring-like structures.

A quasiring is an algebraic structure for which both addition and multiplication
forms a monoid, multiplication distributes over addition and has an annihilating
zero. A quasiring $(Q,+,*,0,1)$ should satisfy the following identities:
\begin{itemize}
  \item $(Q,+,0)$ is a monoid:
  \begin{itemize}
    \item Associativity: $\forall x,y,z \in Q, x + (y + z) = (x + y) + z$
    \item Identity: $\forall x \in Q, (x + 0) = x = (0 + x)$
  \end{itemize}
  \item $(Q,*,1)$ is a monoid:
  \begin{itemize}
    \item Associativity: $ \forall x,y,z \in Q: x * (y*z) = (x*y)*z$
    \item Identity: $\forall x \in Q, (x * 1) = x = (1 * x)$
  \end{itemize}
  \item Multiplication distributes over addition: \(\forall x , y , z \in Q, (x * (y + z)) = (x * y) + (x
  * z)\) and \( (x + y) * z = (x * z) + (y * z) \)
  \item Annihilating zero: \(\forall x \in Q, (x * 0) = 0 = (0 * x)\)
\end{itemize}

\begin{minted}[breaklines,samepage]{Agda}
record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-cong        : Congruent₂ *
    *-assoc       : Associative *
    *-identity    : Identity 1# *
    distrib       : * DistributesOver +
    zero          : Zero 0# *

  open IsMonoid +-isMonoid public
\end{minted}

A quasiring with additive inverse is called a nearring. For the structure
nearring, addition forms a group, multiplication forms a monoid, multiplication
distributes over addition and has an annihilating zero.

\begin{minted}[breaklines,samepage]{Agda}
record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  field
    isQuasiring : IsQuasiring + * 0# 1#
    +-inverse   : Inverse 0# _⁻¹ +
    ⁻¹-cong     : Congruent₁ _⁻¹

  open IsQuasiring isQuasiring public
\end{minted}

A ring without one or rig or ring without unit is an algebraic structure with
two binary operations, a unary and a nullary operation. A ringWithoutOne
$(R,+,*,⁻¹,0)$ should satisfy the following identities:
\begin{itemize}
  \item $(R,+,⁻¹,0)$ is an Abelian Group:
   \begin{itemize}
    \item Associativity: $\forall x,y,z \in R, x + (y + z) = (x + y) + z$
    \item commutativity: $\forall x,y \in R, (x + y) = (y + x)$
    \item Identity: $\forall x \in R, (x + 0) = x = (0 + x)$
    \item Inverse: $\forall x \in R, (x + x⁻¹) = 0 = (x⁻¹ + x)$
  \end{itemize}
  \item $(R,*)$ is a semigroup
  \begin{itemize}
    \item Associativity: $ \forall x,y,z \in R, x * (y*z) = (x*y)*z$
  \end{itemize}
  \item Multiplication distributes over addition: \(\forall x , y , z \in R, (x * (y + z)) = (x * y) + (x
  * z)\) and \( (x + y) * z = (x * z) + (y * z) \)
  \item Annihilating zero: \(\forall x \in R, (x * 0) = 0 = (0 * x)\)
\end{itemize}

\begin{minted}[breaklines,samepage]{Agda}
record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-cong           : Congruent₂ *
    *-assoc          : Associative *
    distrib          : * DistributesOver +
    zero             : Zero 0# *

  open IsAbelianGroup +-isAbelianGroup public
\end{minted}

\section{Homomorphism} 
A structure-preserving map between two structures is called a homomorphism. In
this section, the homomorphism of RingWithoutOne structure is discussed. The
homomorphism for ringWithoutOne structure can be defined using group
homomorphism. For two group structures $(G_1,+_1,^{-1},e_1)$ and
$(G_2,+_2,^{-1},e_2)$, homomorphism $f:(G_1,+_1,^{-1},e_1) \rightarrow
(G_2,+_2,^{-1},e_2)$ is a structure-preserving map such that:
\begin{itemize}
  \item $f$ preserves the binary operation: $f(x +_1 y) = f(x) +_2 f(y)$
  \item $f$ preserves the inverse operation: $f(x⁻¹) = f(x)⁻¹$
  \item $f$ preserves the identity: $f(e_1) = e_2$ where $e_1$ is the identity
  in $G_1$ and $e_2$ is the identity in $G_2$
\end{itemize}
In Agda, homomorphism for ringWithoutOne is defined using group homomorphism
such that for two ringWithoutOne structures $R_1$ and $R_2$, the homomorphism
$f: R_1 \rightarrow R_2$ is a group homomorphism and preserves the
multiplication operation. That is $f$ is a group homomorphism and \(f(x *_1 y) =
f(x) *_2 f(y)\).

\begin{minted}[breaklines,samepage]{Agda}
record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    +-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧
    *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_

  open +.IsGroupHomomorphism +-isGroupHomomorphism public
    renaming (homo to +-homo; ε-homo to 0#-homo;
    isMagmaHomomorphism to +-isMagmaHomomorphism)
\end{minted} 

In the above definition, \inline{IsRingWithoutOneHomomorphism} is defined as a
record type with two fields \inline{+-isGroupHomomorphism} and \inline{*-homo}.
The definition of isomorphism and monomorphism can be found in the Agda standard
library under the module \inline{Algebra.Morphism.Structures}.

\section{Composition of Homomorphism}
If $f$ is a homomorphism such that $f\ :\ a \ \rightarrow \ b$ and $g$ is a
homomorphism such that $g\ :\ b\ \rightarrow \ c$, then composition of
homomorphisms can be defined as $g \ ∘\ f\ :\ a \ \rightarrow \ c$.

\begin{minted}[breaklines,samepage]{Agda}
  isRingWithoutOneHomomorphism
    : IsRingWithoutOneHomomorphism R₁ R₂ f
    → IsRingWithoutOneHomomorphism R₂ R₃ g
    → IsRingWithoutOneHomomorphism R₁ R₃ (g ∘ f)
  isRingWithoutOneHomomorphism f-homo g-homo = record
    { +-isGroupHomomorphism = isGroupHomomorphism ≈₃-trans
		 F.+-isGroupHomomorphism G.+-isGroupHomomorphism
    ; *-homo                 = λ x y → ≈₃-trans 
		(G.⟦⟧-cong (F.*-homo x y)) (G.*-homo (f x) (f y))
    } where module F = IsRingWithoutOneHomomorphism f-homo;
		 module G = IsRingWithoutOneHomomorphism g-homo
\end{minted}
In the above ringWithoutOne homomorphism composition, \inline{f} is a
homomorphism from ringWithoutOne structures $R₁$ to $R₂$, \inline{g} is a
homomorphism from ringWithoutOne structures $R₂$ to $R₃$.
\inline{isGroupHomomorphism} field gives the composition of group homomorphism.
We can define the composition for binary operations homomorphism (*) using
transitive relation \inline{≈₃-trans} from $R₁$ to $R₃$ such that \[g (f ((R₁ * x)
y)) ≈ (g ((R₂ * f x) (f y)) \text{ and } g ((R₂ * f x) (f y))) ≈ ((R₃ * g (f x))
(g (f y)))\]
\[\Rightarrow g (f ((R₁ * x) y)) ≈ ((R₃ * g (f x)) (g (f y)))\]

\section{Product Algebra}
The product of ring-like structures in Agda is defined as:

\begin{minted}[breaklines,samepage]{Agda}
ringWithoutOne : RingWithoutOne a ℓ₁ → 
		RingWithoutOne b ℓ₂ → RingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
ringWithoutOne R S = record
  { isRingWithoutOne = record
      { +-isAbelianGroup = AbelianGroup.isAbelianGroup
		 ((abelianGroup R.+-abelianGroup S.+-abelianGroup))
      ; *-cong           = Semigroup.∙-cong
		 (semigroup R.*-semigroup S.*-semigroup)
      ; *-assoc   = Semigroup.assoc (semigroup R.*-semigroup S.*-semigroup)
      ; distrib     = (λ x y z → 
		(R.distribˡ , S.distribˡ) <*> x <*> y <*> z)
                            , (λ x y z → 
		(R.distribʳ , S.distribʳ) <*> x <*> y <*> z)
      ; zero     = uncurry (λ x y → R.zeroˡ x , S.zeroˡ y)
                            , uncurry (λ x y → R.zeroʳ x , S.zeroʳ y)
      }

  } where module R = RingWithoutOne R; module S = RingWithoutOne S
\end{minted}

The definition of product is similar to quasigroups discussed in Chapter 5. The
definitions of products of \inline{nonAssociativeRing}, \inline{quasiring}, and
\inline{nearring} can be defined similarly to \inline{ringWithoutOne}. These
definitions can be found in the Agda standard library.

\section{Properties}
With these definitions, we can prove some frequently used properties and theories
about the structures.\footnote{This section provides proof for properties that
was contributed by the author and other properties can be found in the Agda standard
library.}
\subsection{Properties Of Semigroup}
Let $(S, ∙)$ be a semigroup then
\begin{enumerate}
\item S is alternative. The Semigroup S left alternative if \((x\ ∙\ x)\ ∙\ y\ =\ x\ ∙\ (x\ ∙\ y)\ \) and right alternative is
\(x\ ∙\ (y\ ∙\ y)\ =\ (x\ ∙\ y)\ ∙\ y\). Semigroup is
said to be alternative if it is both left and right alternative. 
\item S is flexible. The Semigroup S is flexible if \(x\ ∙\ (y\
∙\ x)\ =\ (x\ ∙\ y)\ ∙\ x\).
\item S has Jordan identity. Jordan identity for binary operation ∙ can be
defined on set S as \((x\ ∙\ y)\ ∙\ (x\ ∙\ x)\ =\
x\ ∙\ (y\ ∙\ (x\ ∙\ x)). \)
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
alternativeˡ : LeftAlternative _∙_
alternativeˡ x y = assoc x x y

alternativeʳ : RightAlternative _∙_
alternativeʳ x y = sym (assoc x y y)

alternative : Alternative _∙_
alternative = alternativeˡ , alternativeʳ
\end{minted}
 \item
\begin{minted}[breaklines,samepage]{Agda}
flexible : Flexible _∙_
flexible x y = assoc x y x
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
xy∙xx≈x∙yxx : ∀ x y → (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x))
xy∙xx≈x∙yxx x y = assoc x y ((x ∙ x))
\end{minted}
\end{enumerate}
\subsection{Properties Of Commutative Semigroup}
An application of semimedial property of commutative semigroup is seen in the
study of quasigroups and loops \cite{liaqat2021some}. The proofs in this section
are adapted from \cite{deng2016characterizations}. Let $(S, ∙)$ be a commutative
semigroup then
\begin{enumerate}
\item S is semimedial. The semigroup S is left semimedial if \(
(x\ ∙\ x)\ ∙\ (y\ ∙\ z)\ =\ (x\ ∙\ y)\ ∙\ (x\ ∙\ z) \) and right
semimedial if \( (y\ ∙\ z)\ ∙\ (x\ ∙\ x)\ =\ (y\ ∙\ x)\ ∙\ (z\ ∙\ x) \).
A structure is semimedial if it is both left and right semimedial. 
\item S is middle semimedial. The semigroup S is middle semimedial if
\((x\ ∙\ y)\ ∙\ (z\ ∙\ x)\ =\ (x\ ∙\ z)\ ∙\ (y\ ∙\
x)\)
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
semimedialˡ : LeftSemimedial _∙_
semimedialˡ x y z = begin
(x ∙ x) ∙ (y ∙ z) ≈⟨ assoc x x (y ∙ z) ⟩
x ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (sym (assoc x y z)) ⟩
x ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
x ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
x ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc x y ((x ∙ z))) ⟩
(x ∙ y) ∙ (x ∙ z) ∎

semimedialʳ : RightSemimedial _∙_
semimedialʳ x y z = begin
(y ∙ z) ∙ (x ∙ x) ≈⟨ assoc y z (x ∙ x) ⟩
y ∙ (z ∙ (x ∙ x)) ≈⟨ ∙-congˡ (sym (assoc z x x)) ⟩
y ∙ ((z ∙ x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm z x)) ⟩
y ∙ ((x ∙ z) ∙ x) ≈⟨ ∙-congˡ (assoc x z x) ⟩
y ∙ (x ∙ (z ∙ x)) ≈⟨ sym (assoc y x ((z ∙ x))) ⟩
(y ∙ x) ∙ (z ∙ x) ∎

semimedial : Semimedial _∙_
semimedial = semimedialˡ , semimedialʳ
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
middleSemimedial x y z = begin
  (x ∙ y) ∙ (z ∙ x) ≈⟨ assoc x y ((z ∙ x)) ⟩
  x ∙ (y ∙ (z ∙ x)) ≈⟨ ∙-congˡ (sym (assoc y z x)) ⟩
  x ∙ ((y ∙ z) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm y z)) ⟩
  x ∙ ((z ∙ y) ∙ x) ≈⟨ ∙-congˡ ( assoc z y x) ⟩
  x ∙ (z ∙ (y ∙ x)) ≈⟨ sym (assoc x z ((y ∙ x))) ⟩
  (x ∙ z) ∙ (y ∙ x) ∎
\end{minted}
\end{enumerate}
\subsection{Properties Of Ring Without One}
Let $(R, +, *, -, 0)$ be ring without one structure then:
\begin{enumerate}
\item \(- (x\ *\ y)\ =\ - x\ *\ y\)
\item \(- (x\ *\ y)\ =\ x\ *\ - y\)
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
-‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
-‿distribˡ-* x y = sym $ begin
  - x * y                        
	≈⟨ sym $ +-identityʳ (- x * y) ⟩
  - x * y + 0#                   
	≈⟨ +-congˡ $ sym ( -‿inverseʳ (x * y) ) ⟩
  - x * y + (x * y + - (x * y))  
	≈⟨ sym $ +-assoc (- x * y) (x * y) (- (x * y)) ⟩
  - x * y + x * y + - (x * y)    
	≈⟨ +-congʳ $ sym ( distribʳ y (- x) x ) ⟩
  (- x + x) * y + - (x * y)      
	≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ x ⟩
  0# * y + - (x * y)             
	≈⟨ +-congʳ $ zeroˡ y ⟩
  0# + - (x * y)                 
	≈⟨ +-identityˡ (- (x * y)) ⟩
  - (x * y)                      
	∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
-‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
-‿distribʳ-* x y = sym $ begin
  x * - y                        
	≈⟨ sym $ +-identityˡ (x * (- y)) ⟩
  0# + x * - y                   
	≈⟨ +-congʳ $ sym ( -‿inverseˡ (x * y) ) ⟩
  - (x * y) + x * y + x * - y    
	≈⟨ +-assoc (- (x * y)) (x * y) (x * (- y)) ⟩
  - (x * y) + (x * y + x * - y)  
	≈⟨ +-congˡ $ sym ( distribˡ x y ( - y) )  ⟩
  - (x * y) + x * (y + - y)      
	≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ y ⟩
  - (x * y) + x * 0#             
	≈⟨ +-congˡ $ zeroʳ x ⟩
  - (x * y) + 0#                 
	≈⟨ +-identityʳ (- (x * y)) ⟩
  - (x * y)                      
	∎
\end{minted}
\end{enumerate}
\subsection{Properties Of Ring}
Properties of rings can be found in number theory and algebraic geometry, where
they are used to study algebraic curves, surfaces, and other geometric objects.
They help in understanding the properties of prime numbers, factorization, and
algebraic varieties \cite{pedrouzo2021revisiting}. Let $(R, +, *, -, 0, 1)$ be a
ring structure then
\begin{enumerate}
\item \(- 1\ *\ x\ =\ -x\)
\item \(\text{if}\ x\ +\ x\ =\ 0\ \text{then}\ x\ =\ 0\)
\item \(x\ *\ (y\ -\ z)\ =\ x\ *\ y\ -\ x\ *\ z\)
\item \((y\ -\ z)\ *\ x\ =\ (y\ *\ x)\ -\ (z\ *\ x)\)
\end{enumerate}
Proof:
\begin{enumerate}
\item
\begin{minted}[breaklines,samepage]{Agda}
-1*x≈-x : ∀ x → - 1# * x ≈ - x
-1*x≈-x x = begin
  - 1# * x    ≈⟨ sym (-‿distribˡ-* 1# x ) ⟩
  - (1# * x)  ≈⟨ -‿cong ( *-identityˡ x ) ⟩
  - x         ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0#
x+x≈x⇒x≈0 x eq = begin
  x           ≈⟨ sym(+-identityʳ x) ⟩
  x + 0#      ≈⟨ +-congˡ (sym (-‿inverseʳ x)) ⟩
  x + (x - x) ≈⟨ sym (+-assoc x x (- x)) ⟩
  x + x - x   ≈⟨ +-congʳ(eq) ⟩
  x - x       ≈⟨ -‿inverseʳ x ⟩
  0#          ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z
x[y-z]≈xy-xz x y z = begin
  x * (y - z)      ≈⟨ distribˡ x y (- z) ⟩
  x * y + x * - z  ≈⟨ +-congˡ (sym (-‿distribʳ-* x z)) ⟩
  x * y - x * z    ∎
\end{minted}
\item
\begin{minted}[breaklines,samepage]{Agda}
[y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x)
[y-z]x≈yx-zx x y z = begin
  (y - z) * x      ≈⟨ distribʳ x y (- z) ⟩
  y * x + - z * x  ≈⟨ +-congˡ (sym (-‿distribˡ-* z x)) ⟩
  y * x - z * x    ∎
\end{minted}
\end{enumerate}