case pos
x y : PGame
h : x ⧏ y
⊢ x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x

case neg
x y : PGame
h : ¬x ⧏ y
⊢ x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x
x y : PGame
⊢ x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x
by_cases h : x ⧏ y
no goals
case pos
x y : PGame
h : x ⧏ y
⊢ x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x
exact Or.inl h
case neg.h
x y : PGame
h : ¬x ⧏ y
⊢ (x ≈ y) ∨ y ⧏ x
case neg
x y : PGame
h : ¬x ⧏ y
⊢ x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x
right
case neg.h.inl
x y : PGame
h : ¬x ⧏ y
h' : y < x
⊢ (x ≈ y) ∨ y ⧏ x

case neg.h.inr
x y : PGame
h : ¬x ⧏ y
h' : y ≈ x
⊢ (x ≈ y) ∨ y ⧏ x
case neg.h
x y : PGame
h : ¬x ⧏ y
⊢ (x ≈ y) ∨ y ⧏ x
cases' lt_or_equiv_of_le (PGame.not_lf.1 h) with h' h'
no goals
case neg.h.inl
x y : PGame
h : ¬x ⧏ y
h' : y < x
⊢ (x ≈ y) ∨ y ⧏ x
exact Or.inr h'.lf
no goals
case neg.h.inr
x y : PGame
h : ¬x ⧏ y
h' : y ≈ x
⊢ (x ≈ y) ∨ y ⧏ x
exact Or.inl h'.symm