Monoid Element Commutes with Identity
=====================================

<!--
SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->

This is a trivial proof of the fact that, in a monoid, the identity element commutes
with any other element.  It is provided mainly as a simple example of how proofs look in Eqthy.

Note that this proof provides justifications on each step.  For a proof as simple as this one,
this isn't actually necessary, and if they were omitted, the `eqthy` checker would still be
able to verify that this proof is valid.  Indeed, the names of the axioms could be omitted as well.

    axiom (#id-right) mul(A, e) = A
    axiom (#id-left)  mul(e, A) = A
    axiom (#assoc)    mul(A, mul(B, C)) = mul(mul(A, B), C)

    theorem (#monoid-element-commutes-with-identity)
        mul(A, e) = mul(e, A)
    proof
        A = A                   [by reflexivity]
        mul(A, e) = A           [by #id-right on LHS]
        mul(A, e) = mul(e, A)   [by #id-left on RHS]
    qed