Metatheorem resolving all consequences of Equation1571

[franklindyer]

This is some intermediate work as I work towards #221, which involves a special case of commutative semigroups. But it also includes some metatheorems that could be generally useful for working with associativity.

Includes:

• a convenience function for fully right-associating any operation tree when the operation is associative
• definition and Magma instance of a free semigroup
• proof that evaluation in any semigroup is a homomorphism
• proof that the variable names can be sorted in a free semigroup expression without affecting the evaluated value, so long as the codomain semigroup is commutative
• all of this is combined to write a metatheorem ProveEquation1571Consequence that should be capable of automatically proving any consequence of Equation1571

Any revisions to shorten my proofs or make the naming/notation more convenient is welcome :-)

[pitmonticone]

Thanks! I will review it later.

[pitmonticone]

Thanks @franklindyer! I have just golfed the new proofs in Subgraph.lean.

Let's wait for the CI and then I'll merge.