[Merged by Bors] - feat(SetTheory/Surreal/Basic): add some lemmas for Surreal.mk

[hwatheod]

add some lemmas for Surreal.mk

---

Split out of #14498

This contains all the lemmas in #14278 plus a few more. I was unable to reopen that one (I think I messed something up by doing a force push), so I am creating a new one.

[github-actions]

PR summary 3a8076c41d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ mk_add
+ mk_eq_mk
+ mk_eq_zero
+ mk_lt_mk
+ mk_lt_mk_moveRight
+ mk_moveLeft_lt_mk
+ mk_sub
+ zero_def
+ zero_le_mk
+ zero_lt_mk

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style