\( \def\List{\operatorname{List}} \) \( \def\integer{\operatorname{integer}} \) \( \def\nat{\operatorname{nat}} \) \( \def\Bool{\operatorname{Bool}} \) \( \def\Punct{\operatorname{Punct}} \) \( \def\BT{\operatorname{BT}} \) \( \def\B{\operatorname{B}} \) \( \def\T{\operatorname{T}} \) \( \def\R{\operatorname{R}} \) \( \def\Set{\operatorname{Set}} \) \( \def\Bag{\operatorname{Bag}} \) \( \def\Ring{\operatorname{Ring}} \) \( \def\plug{\operatorname{plug}} \) \( \def\Zipper{\operatorname{Zipper}} \) \( \def\cosh{\operatorname{cosh}} \) \( \def\sinh{\operatorname{sinh}} \) \( \def\ch{\operatorname{ch}} \) \( \def\sh{\operatorname{sh}} \) \( \def\d{\partial} \)
Blindsight spot.

I just realised that in any unital ring commutativity of addition follows from distributivity:

$$$$

\begin{array}{r@{\;}c@{\;}l@{\quad}} a + b &\;=\;& -a + a + a + b + b - b \\ &\;=\;& -a + a\cdot(1 + 1) + b\cdot(1 + 1) - b \\ &\;=\;& -a + (a + b)\cdot(1 + 1) - b \\ &\;=\;& -a + (a + b)\cdot 1 + (a + b)\cdot 1 - b \\ &\;=\;& -a + a + b + a + b - b \\ &\;=\;& b + a \end{array}

The same holds for unital modules, algebras, vector spaces, &c. Note that multiplication doesn't even need to be associative. It's amazing how such things can pass unnoticed.