(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
        )))