feat(set_theory/game/{pgame, basic}): Add more order lemmas (#13807)

src/set_theory/game/basic.lean

@@ -67,6 +67,12 @@ into a `def` instead. -/
 instance : has_lt game :=
 ⟨quotient.lift₂ (λ x y, x < y) (λ x₁ y₁ x₂ y₂ hx hy, propext (lt_congr hx hy))⟩
 
+theorem lt_or_eq_of_le : ∀ {x y : game}, x ≤ y → x < y ∨ x = y :=
+by { rintro ⟨x⟩ ⟨y⟩, change _ → _ ∨ ⟦x⟧ = ⟦y⟧, rw quotient.eq, exact lt_or_equiv_of_le }
+
+instance : is_trichotomous game (<) :=
+⟨by { rintro ⟨x⟩ ⟨y⟩, change _ ∨ ⟦x⟧ = ⟦y⟧ ∨ _, rw quotient.eq, apply lt_or_equiv_or_gt }⟩
+
 @[simp] theorem not_le : ∀ {x y : game}, ¬ x ≤ y ↔ y < x :=
 by { rintro ⟨x⟩ ⟨y⟩, exact not_le }
 

src/set_theory/game/pgame.lean

@@ -526,6 +526,19 @@ theorem le_congr {x₁ y₁ x₂ y₂} : x₁ ≈ x₂ → y₁ ≈ y₂ → (x
 theorem lt_congr {x₁ y₁ x₂ y₂} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ < y₁ ↔ x₂ < y₂ :=
 not_le.symm.trans $ (not_congr (le_congr hy hx)).trans not_le
 
+theorem lt_or_equiv_of_le {x y : pgame} (h : x ≤ y) : x < y ∨ x ≈ y :=
+or_iff_not_imp_left.2 $ λ h', ⟨h, not_lt.1 h'⟩
+
+theorem lt_or_equiv_or_gt (x y : pgame) : x < y ∨ x ≈ y ∨ y < x :=
+begin
+  by_cases h : x < y,
+  { exact or.inl h },
+  { right,
+    cases (lt_or_equiv_of_le (not_lt.1 h)) with h' h',
+    { exact or.inr h' },
+    { exact or.inl h'.symm } }
+end
+
 theorem equiv_congr_left {y₁ y₂} : y₁ ≈ y₂ ↔ ∀ x₁, x₁ ≈ y₁ ↔ x₁ ≈ y₂ :=
 ⟨λ h x₁, ⟨λ h', equiv_trans h' h, λ h', equiv_trans h' (equiv_symm h)⟩,
  λ h, (h y₁).1 $ equiv_refl _⟩