[Question]
  [
We all know that \$(-a) \times (-a) = a \times a\$ (hopefully), but can you prove it?
Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of rules that two binary operations on a set have to follow. The two operation are addition, \$+\$, and multiplication, \$\times\$. For this challenge here are the ring axioms where \$+\$ and \$\times\$ are closed binary operations on some set \$S\$, \$-\$ is a closed unary operation on \$S\$, and \$a\$, \$b\$, \$c\$ are members of \$S\$:
1. \$a + (b + c) = (a + b) + c\$
2. \$a + 0 = a\$
3. \$a + (-a) = 0\$
4. \$a + b = b + a\$\*
5. \$a \times (b \times c) = (a \times b) \times c\$
6. \$a \times 1 = a\$†
7. \$1 × a = a\$†
8. \$a \times (b + c) = (a \times b) + (a × c)\$
9. \$(b + c) \times a = (b \times a) + (c \times a)\$
Your proof should be a string of equalities each being the application of one axiom.
You may apply the axioms to either the entire expression or to some sub-expression. For example if we have \$(a + c) + (b + c)\$ we can apply Axiom 4 to just the \$(b + c)\$ term, the \$(a + c)\$ term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to \$((a \times c) + b) + ((-a) + 1)\$ to get \$((-a) + 1) + ((a \times c) + b)\$. In each step of the proof you can only apply *one* axiom to *one* expression. All axioms are bidirectional, meaning substitution can go in either direction. Things like the following are not allowed
```
(a + b) + (c + d) = (a + (b + c)) + d Ax. 1
```
This should be done in two steps:
```
(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
                  = (a + (b + c)) + d Ax. 1
```
Facts you might normally take for granted but are not listed on the axioms list *cannot be assumed*, for example \$(-a) = (-1) \times a\$ is true but requires multiple steps to preform.
User [Anthony](https://codegolf.stackexchange.com/users/71303/antony) has kindly provided [a online proof validator](https://antony74.github.io/fol/)
 that can be used as a replacement for TIO.
## Example proof
Here is an example proof that \$-(-a) = a\$ with the axioms used labeled on the right of each step.
```
 -(-a) = (-(-a)) + 0          Ax. 2
       = 0 + (-(-a))          Ax. 4
       = (a + (-a)) + (-(-a)) Ax. 3
       = a + ((-a) + (-(-a))) Ax. 1
       = a + 0                Ax. 3
       = a                    Ax. 2
```
[Try it online!](https://antony74.github.io/fol/index.html?eJzT0NXQTdTU5NKA0NoGXAbaGjCxRG2IIEwAyAcxYHyQgAFXIgClkAyv)
You will be tasked to prove \$(-a) \times (-a) = a \times a\$ using successive substitution like that shown above.
## Scoring
This is [proof-golf](/questions/tagged/proof-golf "show questions tagged 'proof-golf'") so your answers will be scored in number of steps taken to get from \$(-a) \times (-a)\$ to \$a \times a\$, with a lower score being better.
### Lemmas
Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion. For the uninitiated, lemmas are proofs of facts that you use later in the proof. In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader. In this challenge using lemmas should not have an direct effect on your score. (Although proof organization may make it easier or harder to golf)
If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it. For example the here is the score breakdown of a proof using lemmas.
```
Lemma:
a × 0 = 0
Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
      = (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
      = ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
      = (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
      = (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
      = (a × b) + (-(a × b))               Ax. 2 (1)
      = 0                                  Ax. 3 (1)
Theorem:
(a × 0) + (b × 0) = 0
Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
                  = (b × 0) + 0  Ax. 4 (1)
                  = b × 0        Ax. 2 (1)
                  = 0            Lemma (7)
```
---
\*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.
†: Since \$1\$ does not appear in the desired equality any proof that uses these axioms is not minimal. That is these axioms cannot help with proving the desired fact. They have been included just for the sake of completeness.
  
[Answer]
## 18 Steps
```
(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
          = ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
          = (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
          = ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
          = ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
          = ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
          = ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
          = (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
          = ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
          = (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
          = (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
          = (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
          = (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
          = (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
          = (a*a)+0                                                   Axiom 3
          = a*a                                                       Axiom 2
```
I wrote a program to check my solution. So if you find an error in this, then my program is wrong too.
[Answer]
## 18 steps
Different from the already posted 18-step solution.
```
a*a = a*a + 0                                                 A2
    = a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
    = (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
    = (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
    = a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
    = a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
    = a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
    = a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
    = a*(-a) + (-(a*(-a) + a*(-a)))                           A2
    = (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
    = (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
    = ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
    = ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
    = ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
    = ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
    = (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
    = (-a)*(-a) + 0                                           A3
    = (-a)*(-a)                                               A2
```
[Answer]
# ~~29~~ 26 Steps
No lemmas!
Comment if you see anything wrong. (It's very easy to make a mistake)
```
(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
            = ((-a) + (a + (-a))) × (-a)                                         Ax. 3
            = ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
            = (a + ((-a) + (-a))) × (-a)                                         Ax. 1
            = (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
            = (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
            = (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
            = (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
            = (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
            = ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
            = (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
            = (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
            = (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
            = (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
            = (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
            = (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
            = (a × a) + (0 × (-a))                                               Ax. 3
            = (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
            = (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
            = (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
            = (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
            = (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
            = (a × a) + 0                                                        Ax. 3
            = (a × a)                                                            Ax. 2
```
Credit goes to [Maltysen](https://codegolf.stackexchange.com/users/31343/maltysen) for **0 × (-a) = 0**
[Answer]
# 18 steps
Not the first 18-step proof, but it’s simpler than the others.
```
(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]
```
[Validate](https://antony74.github.io/fol/index.html?eJyNkcsNACEIRO9bhUd0YzIt2X8TouKPsGQvyucxE5RyiYn4eGhG4Q24MupJ4ShLGBm%252FiFE9CQVM4R9Yd0IzUaDtiA9FAV2miJLDwGwhzdEEPbVEPWb39jqaEmi9iUA2tfbxALWGNji%252Bd7TQ7gosvGmU)
[Answer]
# 23 steps
```
(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
            = ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
            = (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
            = (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
            = (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
            = ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
            = (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
            = ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
            = (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
            = ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
            = ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
            = 0 + -((-a) * a)                                   ✔ axiom 3
            = (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
            = ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
            = ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
            = ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
            = ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
            = (0 * a ) + -((-a) * a)                            ✔ axiom 2
            = ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
            = ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
            = (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
            = (a * a) + 0                                       ✔ axiom 3
            = a * a                                             ✔ axiom 2
```
[Try it online!](https://antony74.github.io/fol/index.html?%28-a%29%20%2a%20%28-a%29%0A%28%28-a%29%20%2a%20%28-a%29%29%20%2B%200%0A%28%28-a%29%20%2a%20%28-a%29%29%20%2B%20%28%28%28-a%29%20%2a%20a%29%20%2B%20-%28%28-a%29%20%2a%20a%29%29%0A%28%28%28-a%29%20%2a%20%28-a%29%29%20%2B%20%28-a%29%20%2a%20a%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28-a%29%20%2a%20%28-a%20%2B%20a%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28-a%29%20%2a%20%28a%20%2B%20%28-a%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28-a%29%20%2a%200%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28%28-a%29%20%2a%200%29%20%2B%200%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28-a%29%20%2a%200%20%2B%20%28%28-a%29%2a0%20%2B%20-%28%28-a%29%2a0%29%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28%28-a%29%20%2a%200%20%2B%20%28-a%29%2a0%29%20%2B%20-%28%28-a%29%2a0%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28-a%29%20%2a%20%280%20%2B%200%29%20%2B%20-%28%28-a%29%2a0%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28-a%29%20%2a%200%20%2B%20-%28%28-a%29%2a0%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A0%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%280%2a%20a%29%20%2B%20-%280%2aa%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%280%2B0%29%2a%20a%29%20%2B%20-%280%2aa%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%280%20%2a%20a%20%29%20%2B%20%280%2aa%29%20%2B%20-%280%2aa%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%280%20%2a%20a%20%29%20%2B%20%28%280%2aa%29%20%2B%20-%280%2aa%29%29%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%280%20%2a%20a%20%29%20%2B%200%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%280%20%2a%20a%20%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28a%20%2B%20-a%29%20%2a%20a%20%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28%28a%20%2a%20a%29%20%2B%20%28-a%29%20%2a%20a%29%20%2B%20-%28%28-a%29%20%2a%20a%29%0A%28a%20%2a%20a%29%20%2B%20%28%28%28-a%29%20%2a%20a%29%20%2B%20-%28%28-a%29%20%2a%20a%29%29%0A%28a%20%2a%20a%29%20%2B%200%0Aa%20%2a%20a%0A%0A)
Yes you read that right, I've written a proof-checker for this puzzle (naturally there's a possibility that the checker itself is wrong)
[Answer]
```
A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)
Lemma: 0 = 0 x a
A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)
```
**~~27~~ 26 steps**
Thank you [Funky Computer Man](https://codegolf.stackexchange.com/users/56656/funky-computer-man) for noticing a duplicate line.
[Answer]
# 304 steps
Community wiki because this proof is generated by Mathematica's [FindEquationalProof](http://reference.wolfram.com/language/ref/FindEquationalProof.html) function.
The proof is rather long. Mathematica doesn't know how to golf it. 
This is the Mathematica code that generates the proof (requires Mathematica 11.3), where `p`, `t`, `n` means `+`, `×`, `-` respectively:
```
ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
   ForAll[a, p[a, 0] == a],
   ForAll[a, p[a, n[a]] == 0],
   ForAll[{a, b}, p[a, b] == p[b, a]],
   ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
   ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
   ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
   ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};
proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];
proof["ProofNotebook"]
```
It is not easy to count the steps directly, so I calculate it by the number of paths from the axioms to the conclusion in the "proof graph".
```
graph = proof["ProofGraph"];
score = Sum[
  Length[FindPath[graph, axiom, "Conclusion 1", Infinity, 
    All]], {axiom, 
   Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]
```
[Try it online!](https://tio.run/##dVJdS8NAEHzvr1hO8ClQ@6oU/BZBpVLx5TzKJT2bw@QuJluoFP3rdXeTauoHhOQyu7Mzc3elxdyVFn1mN5vah8XJyseygTGsL2N9UhR6bRNIE8jeE6i05Rf/GQPjMa0FSo0gyQAAOpbtug@kz/5ZC9q2Yw52yiK4VUs7HdK05ndb6wu5E3u@UOP/vqQ02vraKYxY5bfhn1K7W/AlJQuC/@d2xK0KcyUY1zJJaN6PBoOqjvGZjuDSh/nF65JOJwZbTBglBm9bb/NElZHv0zM0Y1HbKqcZMksrIV8xprg6oWbU02Wp2eqNCwvMNctN6D5o4dJQHpaAOoshK5YNmYCRSuA6PPvg8S0B5gJQSooM665dwKkrXIb60dXoVje@wXYmtU2Rfd5azPJ7rcQvKPj4gNmMwhvhK2jQVc1T6HlVD7lvgB66r20oWLjgaotuDumbwFmcu8NdFpshz3sG9mF4zMPPyRq6M9u4RsKf17HSratpVXjUbarrsoo1tngHwcWqh/U39i6iS2N8UeRf3Z3yZ83f7RaRh0lhyZBboeKQil3yLeQlKgPDIdwvvcPN5hM "Wolfram Language (Mathematica) – Try It Online")
This is the proof generated by the code:
```
Axiom 1
We are given that:
x1==p[x1, 0]
Axiom 2
We are given that:
x1==t[x1, 1]
Axiom 3
We are given that:
x1==t[1, x1]
Axiom 4
We are given that:
p[x1, x2]==p[x2, x1]
Axiom 5
We are given that:
p[x1, p[x2, x3]]==p[p[x1, x2], x3]
Axiom 6
We are given that:
p[x1, n[x1]]==0
Axiom 7
We are given that:
p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]
Axiom 8
We are given that:
p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]
Axiom 9
We are given that:
t[x1, t[x2, x3]]==t[t[x1, x2], x3]
Hypothesis 1
We would like to show that:
t[n[a], n[a]]==t[a, a]
Critical Pair Lemma 1
The following expressions are equivalent:
p[0, x1]==x1
Proof
Note that the input for the rule:
p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, 0]->x1
where these rules follow from Axiom 4 and Axiom 1 respectively.
Critical Pair Lemma 2
The following expressions are equivalent:
p[x1, p[n[x1], x2]]==p[0, x2]
Proof
Note that the input for the rule:
p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, n[x1_]]->0
where these rules follow from Axiom 5 and Axiom 6 respectively.
Critical Pair Lemma 3
The following expressions are equivalent:
t[p[1, x1], x2]==p[x2, t[x1, x2]]
Proof
Note that the input for the rule:
p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]
contains a subpattern of the form:
t[x1_, x2_]
which can be unified with the input for the rule:
t[1, x1_]->x1
where these rules follow from Axiom 7 and Axiom 3 respectively.
Critical Pair Lemma 4
The following expressions are equivalent:
t[x1, p[1, x2]]==p[x1, t[x1, x2]]
Proof
Note that the input for the rule:
p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]
contains a subpattern of the form:
t[x1_, x2_]
which can be unified with the input for the rule:
t[x1_, 1]->x1
where these rules follow from Axiom 8 and Axiom 2 respectively.
Critical Pair Lemma 5
The following expressions are equivalent:
t[p[1, x1], 0]==t[x1, 0]
Proof
Note that the input for the rule:
p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]
contains a subpattern of the form:
p[x1_, t[x2_, x1_]]
which can be unified with the input for the rule:
p[0, x1_]->x1
where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.
Critical Pair Lemma 6
The following expressions are equivalent:
t[0, 0]==t[1, 0]
Proof
Note that the input for the rule:
t[p[1, x1_], 0]->t[x1, 0]
contains a subpattern of the form:
p[1, x1_]
which can be unified with the input for the rule:
p[x1_, 0]->x1
where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.
Substitution Lemma 1
It can be shown that:
t[0, 0]==0
Proof
We start by taking Critical Pair Lemma 6, and apply the substitution:
t[1, x1_]->x1
which follows from Axiom 3.
Critical Pair Lemma 7
The following expressions are equivalent:
t[x1, 0]==t[p[x1, 1], 0]
Proof
Note that the input for the rule:
t[p[1, x1_], 0]->t[x1, 0]
contains a subpattern of the form:
p[1, x1_]
which can be unified with the input for the rule:
p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]
where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.
Critical Pair Lemma 8
The following expressions are equivalent:
t[0, p[1, x1]]==t[0, x1]
Proof
Note that the input for the rule:
p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]
contains a subpattern of the form:
p[x1_, t[x1_, x2_]]
which can be unified with the input for the rule:
p[0, x1_]->x1
where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.
Critical Pair Lemma 9
The following expressions are equivalent:
t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]
Proof
Note that the input for the rule:
p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]
contains a subpattern of the form:
t[x1_, x2_]
which can be unified with the input for the rule:
t[p[x1_, 1], 0]->t[x1, 0]
where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.
Substitution Lemma 2
It can be shown that:
t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]
Proof
We start by taking Critical Pair Lemma 9, and apply the substitution:
p[x1_, 0]->x1
which follows from Axiom 1.
Substitution Lemma 3
It can be shown that:
p[x1, 1]==p[p[x1, 1], t[x1, 0]]
Proof
We start by taking Substitution Lemma 2, and apply the substitution:
t[x1_, 1]->x1
which follows from Axiom 2.
Substitution Lemma 4
It can be shown that:
p[x1, 1]==p[x1, p[1, t[x1, 0]]]
Proof
We start by taking Substitution Lemma 3, and apply the substitution:
p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]
which follows from Axiom 5.
Critical Pair Lemma 10
The following expressions are equivalent:
t[0, x1]==t[0, p[x1, 1]]
Proof
Note that the input for the rule:
t[0, p[1, x1_]]->t[0, x1]
contains a subpattern of the form:
p[1, x1_]
which can be unified with the input for the rule:
p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]
where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.
Critical Pair Lemma 11
The following expressions are equivalent:
t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]
Proof
Note that the input for the rule:
p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]
contains a subpattern of the form:
t[x2_, x1_]
which can be unified with the input for the rule:
t[0, p[x1_, 1]]->t[0, x1]
where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.
Substitution Lemma 5
It can be shown that:
t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]
Proof
We start by taking Critical Pair Lemma 11, and apply the substitution:
p[x1_, 0]->x1
which follows from Axiom 1.
Substitution Lemma 6
It can be shown that:
p[x1, 1]==p[p[x1, 1], t[0, x1]]
Proof
We start by taking Substitution Lemma 5, and apply the substitution:
t[1, x1_]->x1
which follows from Axiom 3.
Substitution Lemma 7
It can be shown that:
p[x1, 1]==p[x1, p[1, t[0, x1]]]
Proof
We start by taking Substitution Lemma 6, and apply the substitution:
p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]
which follows from Axiom 5.
Substitution Lemma 8
It can be shown that:
p[x1, p[n[x1], x2]]==x2
Proof
We start by taking Critical Pair Lemma 2, and apply the substitution:
p[0, x1_]->x1
which follows from Critical Pair Lemma 1.
Critical Pair Lemma 12
The following expressions are equivalent:
n[n[x1]]==p[x1, 0]
Proof
Note that the input for the rule:
p[x1_, p[n[x1_], x2_]]->x2
contains a subpattern of the form:
p[n[x1_], x2_]
which can be unified with the input for the rule:
p[x1_, n[x1_]]->0
where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.
Substitution Lemma 9
It can be shown that:
n[n[x1]]==x1
Proof
We start by taking Critical Pair Lemma 12, and apply the substitution:
p[x1_, 0]->x1
which follows from Axiom 1.
Critical Pair Lemma 13
The following expressions are equivalent:
x1==p[n[x2], p[x2, x1]]
Proof
Note that the input for the rule:
p[x1_, p[n[x1_], x2_]]->x2
contains a subpattern of the form:
n[x1_]
which can be unified with the input for the rule:
n[n[x1_]]->x1
where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.
Critical Pair Lemma 14
The following expressions are equivalent:
t[x1, x2]==p[n[x2], t[p[1, x1], x2]]
Proof
Note that the input for the rule:
p[n[x1_], p[x1_, x2_]]->x2
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]
where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.
Critical Pair Lemma 15
The following expressions are equivalent:
t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]
Proof
Note that the input for the rule:
p[n[x1_], p[x1_, x2_]]->x2
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]
where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.
Critical Pair Lemma 16
The following expressions are equivalent:
p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]
Proof
Note that the input for the rule:
p[n[x1_], p[x1_, x2_]]->x2
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]
where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.
Substitution Lemma 10
It can be shown that:
p[1, t[x1, 0]]==1
Proof
We start by taking Critical Pair Lemma 16, and apply the substitution:
p[n[x1_], p[x1_, x2_]]->x2
which follows from Critical Pair Lemma 13.
Critical Pair Lemma 17
The following expressions are equivalent:
t[t[x1, 0], 0]==t[1, 0]
Proof
Note that the input for the rule:
t[p[1, x1_], 0]->t[x1, 0]
contains a subpattern of the form:
p[1, x1_]
which can be unified with the input for the rule:
p[1, t[x1_, 0]]->1
where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.
Substitution Lemma 11
It can be shown that:
t[x1, t[0, 0]]==t[1, 0]
Proof
We start by taking Critical Pair Lemma 17, and apply the substitution:
t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]
which follows from Axiom 9.
Substitution Lemma 12
It can be shown that:
t[x1, 0]==t[1, 0]
Proof
We start by taking Substitution Lemma 11, and apply the substitution:
t[0, 0]->0
which follows from Substitution Lemma 1.
Substitution Lemma 13
It can be shown that:
t[x1, 0]==0
Proof
We start by taking Substitution Lemma 12, and apply the substitution:
t[1, x1_]->x1
which follows from Axiom 3.
Critical Pair Lemma 18
The following expressions are equivalent:
t[x1, t[0, x2]]==t[0, x2]
Proof
Note that the input for the rule:
t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]
contains a subpattern of the form:
t[x1_, x2_]
which can be unified with the input for the rule:
t[x1_, 0]->0
where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.
Critical Pair Lemma 19
The following expressions are equivalent:
p[1, t[0, x1]]==p[n[x1], p[x1, 1]]
Proof
Note that the input for the rule:
p[n[x1_], p[x1_, x2_]]->x2
contains a subpattern of the form:
p[x1_, x2_]
which can be unified with the input for the rule:
p[x1_, p[1, t[0, x1_]]]->p[x1, 1]
where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.
Substitution Lemma 14
It can be shown that:
p[1, t[0, x1]]==1
Proof
We start by taking Critical Pair Lemma 19, and apply the substitution:
p[n[x1_], p[x1_, x2_]]->x2
which follows from Critical Pair Lemma 13.
Critical Pair Lemma 20
The following expressions are equivalent:
t[0, t[0, x1]]==t[0, 1]
Proof
Note that the input for the rule:
t[0, p[1, x1_]]->t[0, x1]
contains a subpattern of the form:
p[1, x1_]
which can be unified with the input for the rule:
p[1, t[0, x1_]]->1
where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.
Substitution Lemma 15
It can be shown that:
t[0, x1]==t[0, 1]
Proof
We start by taking Critical Pair Lemma 20, and apply the substitution:
t[x1_, t[0, x2_]]->t[0, x2]
which follows from Critical Pair Lemma 18.
Substitution Lemma 16
It can be shown that:
t[0, x1]==0
Proof
We start by taking Substitution Lemma 15, and apply the substitution:
t[x1_, 1]->x1
which follows from Axiom 2.
Critical Pair Lemma 21
The following expressions are equivalent:
t[n[1], x1]==p[n[x1], t[0, x1]]
Proof
Note that the input for the rule:
p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]
contains a subpattern of the form:
p[1, x2_]
which can be unified with the input for the rule:
p[x1_, n[x1_]]->0
where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.
Substitution Lemma 17
It can be shown that:
t[n[1], x1]==p[n[x1], 0]
Proof
We start by taking Critical Pair Lemma 21, and apply the substitution:
t[0, x1_]->0
which follows from Substitution Lemma 16.
Substitution Lemma 18
It can be shown that:
t[n[1], x1]==n[x1]
Proof
We start by taking Substitution Lemma 17, and apply the substitution:
p[x1_, 0]->x1
which follows from Axiom 1.
Critical Pair Lemma 22
The following expressions are equivalent:
t[n[1], t[x1, x2]]==t[n[x1], x2]
Proof
Note that the input for the rule:
t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]
contains a subpattern of the form:
t[x1_, x2_]
which can be unified with the input for the rule:
t[n[1], x1_]->n[x1]
where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.
Substitution Lemma 19
It can be shown that:
n[t[x1, x2]]==t[n[x1], x2]
Proof
We start by taking Critical Pair Lemma 22, and apply the substitution:
t[n[1], x1_]->n[x1]
which follows from Substitution Lemma 18.
Critical Pair Lemma 23
The following expressions are equivalent:
t[x1, n[1]]==p[n[x1], t[x1, 0]]
Proof
Note that the input for the rule:
p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]
contains a subpattern of the form:
p[1, x2_]
which can be unified with the input for the rule:
p[x1_, n[x1_]]->0
where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.
Substitution Lemma 20
It can be shown that:
t[x1, n[1]]==p[n[x1], 0]
Proof
We start by taking Critical Pair Lemma 23, and apply the substitution:
t[x1_, 0]->0
which follows from Substitution Lemma 13.
Substitution Lemma 21
It can be shown that:
t[x1, n[1]]==n[x1]
Proof
We start by taking Substitution Lemma 20, and apply the substitution:
p[x1_, 0]->x1
which follows from Axiom 1.
Critical Pair Lemma 24
The following expressions are equivalent:
n[t[x1, x2]]==t[x1, t[x2, n[1]]]
Proof
Note that the input for the rule:
t[x1_, n[1]]->n[x1]
contains a subpattern of the form:
t[x1_, n[1]]
which can be unified with the input for the rule:
t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]
where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.
Substitution Lemma 22
It can be shown that:
t[n[x1], x2]==t[x1, t[x2, n[1]]]
Proof
We start by taking Critical Pair Lemma 24, and apply the substitution:
n[t[x1_, x2_]]->t[n[x1], x2]
which follows from Substitution Lemma 19.
Substitution Lemma 23
It can be shown that:
t[n[x1], x2]==t[x1, n[x2]]
Proof
We start by taking Substitution Lemma 22, and apply the substitution:
t[x1_, n[1]]->n[x1]
which follows from Substitution Lemma 21.
Substitution Lemma 24
It can be shown that:
t[a, n[n[a]]]==t[a, a]
Proof
We start by taking Hypothesis 1, and apply the substitution:
t[n[x1_], x2_]->t[x1, n[x2]]
which follows from Substitution Lemma 23.
Conclusion 1
We obtain the conclusion:
True
Proof
Take Substitution Lemma 24, and apply the substitution:
n[n[x1_]]->x1
which follows from Substitution Lemma 9.
```
[Answer]
# 6 + 7 + 7 + 6 + 3 = 29 steps
I really hope I didn't screw anything up, leave a comment if you think I did.
```
Lemma 1. a*0=0 (6 steps)
0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2
Lemma 2. a*(-b) = -(a*b) (7 steps)
a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2
Lemma 3. (-a)*b = -(a*b) (7 steps)
    same as above
Lemma 4. -(-(a)) = a (6 steps)
 -(-a) = (-(-a)) + 0    axiom 2
 = 0 + (-(-a))          axiom 4
 = (a + (-a)) + (-(-a)) axiom 3
 = a + ((-a) + (-(-a))) axiom 1
 = a + 0                axiom 3
 = a                    axiom 2
Theorem. -a*-a=0 (3 steps)
-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4
Q.E.D.
```
[Answer]
## ~~22~~ 23 Steps
New answer, as my previous was flawed. Let me add some general comments first:
* The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string.
* Multiplication is not assumed to be commutative.
* We are given a unit **1**, but it plays no role whatsoever in the puzzle because it is involved exclusively in the rules that define it.
Now for the proof (notice I define **n = (-a)** to simplify reading):
```
(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]
```
[Answer]
# 34 steps
```
Lemma 1: 0=0*a (8 steps)
    0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0
Theorem: -a*-a = a*a (49 steps)
    -a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a
```
[Answer]
# 25 steps
Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly.
**Lemma Z** *[6 steps]*: `0*a = 0`:
```
0 = (0*a) + (-(0*a))       | Ax. 3
  = ((0+0)*a) + (-(0*a))   | Ax. 2
  = (0*a + 0*a) + (-(0*a)) | Ax. 9
  = 0*a + (0*a + (-(0*a))) | Ax. 1
  = 0*a + (0)              | Ax. 3
  = 0*a                    | Ax. 2
```
**Lemma M** *[12 steps]*: `(-a)*b = -(a*b)`
```
(-a)*b = (-a)*b + 0                | Ax. 2
       = (-a)*b + (a*b + (-(a*b))) | Ax. 3
       = ((-a)*b + a*b) + (-(a*b)) | Ax. 5
       = ((-a)+a)*b + (-(a*b))     | Ax. 9
       = 0*b + (-(a*b))            | Ax. 3
       = 0 + (-(a*b))              | Lem. Z [6]
       = -(a*b)                    | Ax. 2
```
**Theorem** *[25 steps]*: `(-a)*(-a) = a*a`
```
(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
          = 0 + (-a)*(-a)                | Ax. 4
          = (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
          = a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
          = a*a + ((-a)*a + (-a)*(-a))   | Lem. M [12]
          = a*a + ((-a)*(a + (-a)))      | Ax. 8
          = a*a + ((-a)*0)               | Ax. 3
          = a*a + 0                      | Lem. Z [6]
          = a*a                          | Ax. 2
```
I feel like there's room for improvement here; for example, I use the commutative property of addition, though it feels like that should be unnecessary, since `(-a)*(-a) = a*a` is true in algebraic structures where addition is non-commutative. On the other hand, in those structures, the additive identity is commutative, and that's all I needed for the proof. I dunno. More generally, the proof's structure seems rather directionless; I just sort of threw stuff at the problem until it worked, so I bet there's some optimization to be done.
This was fun--thanks for the interesting and creative question OP! I haven't seen challenges like these before; hopefully [proof-golf](/questions/tagged/proof-golf "show questions tagged 'proof-golf'") becomes a thing!
]