This is an experimental approach to make it clearer (and easier) to do basic algebra in set.mm.
These little theorems support basic algebra on equations at a slightly higher conceptual level. Instead of always having to "build up" equivalent expressions for one side of an equation, these theorems allow you to directly manipulate an equality. These higher-level steps lead to easier to understand proofs when they can be used, as well as proofs that are slightly shorter (when measured in steps).
There are disadvantages. In particular, this approach requires many theorems (for many permutations to provide all of the operations). It can also only handle certain cases; more complex approaches must still be approached by "building up" equalities as is done today.
However, I expect that we can create enough theorems to make it worth doing. I'm trying this out to see if this is helpful and if the number of permutations is manageable.
To commute LHS for addition, use addcomli. We might want to switch to a naming convention like addcomli.