x y : PGame
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
x y : PGame
⊢ x < y ∨ (x ≈ y) ∨ y ⧏ x
rw [lf_iff_lt_or_fuzzy, Fuzzy.swap_iff]
no goals
x y : PGame
⊢ x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y
exact lt_or_equiv_or_gt_or_fuzzy x y