```
(def-theorem associative-law-for-multiplication-for-monoids
Remark: This entry is multiply defined. See:  [1] [2]
associative-law-for-multiplication-for-monoids
(usages transportable-macete)
(theory monoid-theory)
(proof existing-theorem))
```

```
(def-theorem reverse-associative-law-for-multiplication-for-monoids
"forall(z,y,x:uu, (x**y)**z = x**(y**z))"
(theory monoid-theory)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)
simplify
)))
```

```
(def-theorem left-cancellation-law-for-monoids
"forall(x,y,z:uu, y = z implies x**y = x**z)"
(theory monoid-theory)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
)
))
```

```
(def-theorem right-cancellation-law-for-monoids
"forall(x,y,z:uu, x = y implies x**z = y**z)"
(usages transportable-macete)
(theory monoid-theory)
(proof
(
direct-and-antecedent-inference-strategy
)
))
```

```
(def-compound-macete monoid-cancellation-laws
(series
(repeat
reverse-associative-law-for-multiplication-for-monoids
tr%reverse-associative-law-for-multiplication-for-monoids)
(repeat
left-cancellation-law-for-monoids
tr%left-cancellation-law-for-monoids)
(repeat
associative-law-for-multiplication-for-monoids
tr%associative-law-for-multiplication-for-monoids)
(repeat
right-cancellation-law-for-monoids
tr%right-cancellation-law-for-monoids)))

```

```
(def-theorem monoid%prod-distributes-over-**
"forall(m,n:zz,f,g:[zz,uu],
m<=n and forall(k:zz, m<=k and k<=n implies #(f(k)) and #(g(k)))
implies
monoid%prod(m,n,lambda(i:zz,f(i)**g(i))) =
monoid%prod(m,n,f) ** monoid%prod(m,n,g))"
(theory commutative-monoid-theory)
(usages transportable-macete)
(proof
(
(induction integer-inductor ("n"))
(backchain "with(p:prop,p implies p)")
direct-and-antecedent-inference-strategy
simplify
simplify
(apply-macete-with-minor-premises monoid-cancellation-laws)
(apply-macete-locally commutative-law-for-monoids
(0)
"monoid%prod(m,t,g)**f(1+t)")
simplify
simplify
simplify
)))
```