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


This file

Going home