Is there a short proof of $x^2=(-x)^2$ in an arbitrary ring?

Identity: Let $R$ be a ring and $x \in R$. Then $x^2=(-x)^2.$

It's exam marking time here, and one of the students used the above identity in a proof. The identity is true, but I can't think of a straightforward proof of this.

Question: Is there a short proof of this identity? (Note: $R$ might not have a multiplicative identity.)

Here's a proof generated by Prover9, which makes me think there might not be a shorter proof. However, this might not necessarily be true, since Prover9 can only work with the ring theory axioms I input (and would have to prove any auxiliary lemmata we would take for granted).

============================== PROOF =================================

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 26.
% Level of proof is 10.
% Maximum clause weight is 16.
% Given clauses 30.

1 x * x = -x * -x # label(non_clause) # label(goal).  [goal].
2 x + (y + z) = (x + y) + z.  [assumption].
3 (x + y) + z = x + (y + z).  [copy(2),flip(a)].
4 x + 0 = x.  [assumption].
5 0 + x = x.  [assumption].
6 x + -x = 0.  [assumption].
8 x + y = y + x.  [assumption].
10 x * (y + z) = (x * y) + (x * z).  [assumption].
11 (x + y) * z = (x * z) + (y * z).  [assumption].
12 -c1 * -c1 != c1 * c1.  [deny(1)].
13 x + (-x + y) = y.  [para(6(a,1),3(a,1,1)),rewrite([5(2)]),flip(a)].
18 (x * 0) + (x * y) = x * y.  [para(5(a,1),10(a,1,2)),flip(a)].
19 (x * y) + (x * -y) = x * 0.  [para(6(a,1),10(a,1,2)),flip(a)].
24 --x = x.  [para(6(a,1),13(a,1,2)),rewrite([4(2)]),flip(a)].
25 x + (y + -x) = y.  [para(8(a,1),13(a,1,2))].
27 (x * y) + ((-x * y) + (z * y)) = z * y.  [para(13(a,1),11(a,1,1)),rewrite([11(5)]),flip(a)].
33 -x + (y + x) = y.  [para(24(a,1),25(a,1,2,2))].
40 x + -(x + y) = -y.  [para(33(a,1),33(a,1,2)),rewrite([8(3)])].
57 -(x + y) = -y + -x.  [para(33(a,1),40(a,1,2,1)),flip(a)].
69 x * 0 = 0.  [para(18(a,1),33(a,1,2)),rewrite([8(4),6(4)]),flip(a)].
70 (x * y) + (x * -y) = 0.  [back_rewrite(19),rewrite([69(6)])].
78 -(x * -y) = x * y.  [para(70(a,1),33(a,1,2)),rewrite([8(5),5(5)])].
87 x * -y = -(x * y).  [para(78(a,1),24(a,1,1)),flip(a)].
88 -(-c1 * c1) != c1 * c1.  [back_rewrite(12),rewrite([87(5)])].
101 -(-x * y) = x * y.  [para(27(a,1),33(a,1,2)),rewrite([57(5),8(8),13(8)])].
102 $F.  [resolve(101,a,88,a)].

============================== end of proof ==========================

Solution 1:

Let $\rm\:y=x\:$ in the Law of Signs: $\rm\:xy = xy+(x+-x)(-y) = x(y+-y) + (-x)(-y) = (-x)(-y)$

Remark $\ $ The proof has the following conceptual intepretation: $\rm\:xy = (-x)(-y)\:$ since they are both additive inverses of $\rm\:x(-y)\:$ hence are equal by uniqueness of inverses. As I frequently emphasize, uniqueness theorems provide powerful tools for proving equalities.

Solution 2:

\begin{align} 0=(x-x)^2 &= x^2+x(-x)+(-x)x+(-x)^2 \\ &= x^2+x(-x)+(-x)x+x^2-x^2+(-x)^2 \\ &= x(x-x)+(-x+x)x-x^2+(-x)^2 \\ &= -x^2+(-x)^2 \end{align}

Solution 3:

what about $x^2-(-x)^2 = (x-(-x))*(x+(-x)) = (x-(-x))*0 = 0$ ?