Surreal dyadic 2 (#4991)

* added addsbday

* shorten addsbday with addsbdaylem

* add addhalfcut

* add pw2cut

* begin working on even/odd theorems

* note move of naddsuc2

* add natural addition closure over _om

* finished zpw2fin

* rewrap

* got madefi and oldfi added

* added cutmax and cutmin

* improve naming consistency

* add missing DV conditions

* get rid of zpw2bday

* proved peano2ons

* added onaddscl, onmulscl, shortened peano2ons

* rewrap

* s/zsmulcld/zmulscld/

---------

Co-authored-by: Fenton <[email protected]>

Author: sctfn

changes-set.txt

@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+20-Aug-25 naddsuc2  [same]      Moved from RP's mathbox to main set.mm
 18-Aug-25 cbvsumi   ---         deleted - redundant with cbvsum
 18-Aug-25 cbvsum    [same]      Removed unneeded hypotheses
 17-Aug-25 bj-denotes iseqsetv-clel Moved from BJ's mathbox to main