Surreals 3 (metamath#4146)

* add lrold

* rewrap

* Shorten nosup/infprefixmo

* work out madebday, oldbday, lrcut, and a few related theorems

* rewrap

* moved rabeqdca

* typo fix

* get surreal induction of one variable working

* define surreal recursion on one variable!

* set up conditions for double recursion on surreals

* Prove noxpordpred

* Begin work on surreal ring operations

* get double induction on surreals going

* got surreal addition commutations!

* Update comments

* move brsnop up

* Fix location of brsnop

* rewrap

Author: sctfn

changes-set.txt

@@ -99,6 +99,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+20-Aug-24 brsnop    [same]	moved from TA's mathbox to main set.mm
 19-Aug-24 dfrp2     [same]      moved from TA's mathbox to main set.mm
 19-Aug-24 rabeqcda  [same]	moved from SN's mathbox to main set.mm
 18-Aug-24 prdsco    [same]      revised - compatibility with new df-prds