feat(set_theory/game/birthday): More basic lemmas on birthdays (#13729)

src/set_theory/game/birthday.lean

@@ -88,11 +88,24 @@ theorem relabelling.birthday_congr : ∀ {x y : pgame.{u}}, relabelling x y →
 end
 using_well_founded { dec_tac := pgame_wf_tac }
 
+@[simp] theorem birthday_add_zero (x : pgame) : birthday (x + 0) = birthday x :=
+(add_zero_relabelling x).birthday_congr
+
+@[simp] theorem birthday_zero_add (x : pgame) : birthday (0 + x) = birthday x :=
+(zero_add_relabelling x).birthday_congr
+
 @[simp] theorem birthday_eq_zero (x : pgame) :
   birthday x = 0 ↔ is_empty x.left_moves ∧ is_empty x.right_moves :=
 by rw [birthday_def, ordinal.max_eq_zero, ordinal.lsub_eq_zero_iff, ordinal.lsub_eq_zero_iff]
 
 @[simp] theorem birthday_zero : birthday 0 = 0 :=
 by { rw birthday_eq_zero, split; apply_instance }
 
+@[simp] theorem birthday_one : birthday 1 = 1 :=
+begin
+  have : (λ i, (move_left 1 i).birthday) = λ i, 0 := funext (λ x, by simp),
+  rw [birthday_def, @ordinal.lsub_empty (right_moves 1), this, ordinal.lsub_const, zero_add],
+  exact max_bot_right 1
+end
+
 end pgame

src/set_theory/game/pgame.lean

@@ -840,6 +840,8 @@ end
 
 instance : has_add pgame := ⟨add⟩
 
+@[simp] theorem nat_one : ((1 : ℕ) : pgame) = 0 + 1 := rfl
+
 /-- `x + 0` has exactly the same moves as `x`. -/
 def add_zero_relabelling : Π (x : pgame.{u}), relabelling (x + 0) x
 | (mk xl xr xL xR) :=