feat(src/set_theory/surreal): add numeric_add and numeric_omega lemmas (#7179)

Adds a couple of lemmas about surreal numbers: proving that natural numbers and omega are numeric.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Surreal.20numbers/near/234243582)

Author: apurvnakade

src/set_theory/surreal.lean

@@ -253,9 +253,14 @@ theorem numeric_add : Π {x y : pgame} (ox : numeric x) (oy : numeric y), numeri
  end⟩
 using_well_founded { dec_tac := pgame_wf_tac }
 
--- TODO prove
--- theorem numeric_nat (n : ℕ) : numeric n := sorry
--- theorem numeric_omega : numeric omega := sorry
+/-- Pre-games defined by natural numbers are numeric. -/
+theorem numeric_nat : Π (n : ℕ), numeric n
+| 0 := numeric_zero
+| (n + 1) := numeric_add (numeric_nat n) numeric_one
+
+/-- The pre-game omega is numeric. -/
+theorem numeric_omega : numeric omega :=
+⟨by rintros ⟨⟩ ⟨⟩, λ i, numeric_nat i.down, by rintros ⟨⟩⟩
 
 end pgame