# Algebraic reflection with a neutral element

Using the tactic for proofs by associativity as a guideline (see in
the example file) to design a tactic by reflection
that compares two algebraic expressions modulo associativity and the
properties of a neutral element. It should be able to prove
equalities of the form `((x+0)+(y+(z+0)))=x+(y+(z+0))`.

## Solution

This file

Going home