From adaed157d74e56ffb45b655974592bd3586fee3b Mon Sep 17 00:00:00 2001
From: Scott Fenton <sctfen@gmail.com>
Date: Mon, 20 Jan 2025 20:29:41 -0500
Subject: [PATCH] add nadd32

---
 set.mm | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/set.mm b/set.mm
index c33a4d3985..f38df7f745 100644
--- a/set.mm
+++ b/set.mm
@@ -539980,6 +539980,14 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
       GVEVFVHDEFURUSYBVKUUIKYIGVEVFVHDEFUTUSVAVBVD $.
   $}
 
+  $( Commutative/associative law that swaps the last two terms in a triple
+     sum.  (Contributed by Scott Fenton, 20-Jan-2025.) $)
+  nadd32 $p |- ( ( A e. On /\ B e. On /\ C e. On ) ->
+  ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) $=
+    ( con0 wcel w3a cnadd co wceq naddcom 3adant1 oveq2d naddass 3com23 3eqtr4d
+    ) ADEZBDEZCDEZFZABCGHZGHACBGHZGHZABGHCGHACGHBGHZSTUAAGQRTUAIPBCJKLABCMPRQUC
+    UBIACBMNO $.
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Surreal numbers - cuts and options