x : PGame
⊢ ((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, moveRight x j ≤ 0) ↔ ∃ j, moveRight x j ≤ 0
x : PGame
⊢ x ⧏ 0 ↔ ∃ j, moveRight x j ≤ 0
rw [lf_iff_exists_le]
no goals
x : PGame
⊢ ((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, moveRight x j ≤ 0) ↔ ∃ j, moveRight x j ≤ 0
simp