x y : PGame
⊢ ¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y
x y : PGame
⊢ x ⧏ y ↔ x < y ∨ x ‖ y
simp only [lt_iff_le_and_lf, Fuzzy, ← PGame.not_le]
no goals
x y : PGame
⊢ ¬y ≤ x ↔ x ≤ y ∧ ¬y ≤ x ∨ ¬y ≤ x ∧ ¬x ≤ y
tauto