v1.0.0

This initial release includes definitions and theorems for algebraic structures ranging from monoids to fields. It includes proofs of all of the basic theorems that apply to these structures and includes expression simplifiers for monoids and groups. The expression simplifier for groups does not yet simplify negations, but provides a basis for further development.

This release satisfies its initial goals by providing a substantial worked example illustrating a functional programming style in Coq and by showing how proof by reflection can be used to automate routine algebraic rewrite steps when developing proofs in this manner.