Monoid Element Commutes with Identity

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