x : PGame
⊢ ((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : RightMoves x), 0 ⧏ moveRight x j) ↔
    ∀ (j : RightMoves x), 0 ⧏ moveRight x j
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : RightMoves x), 0 ⧏ moveRight x j
rw [le_iff_forall_lf]
no goals
x : PGame
⊢ ((∀ (i : LeftMoves 0), moveLeft 0 i ⧏ x) ∧ ∀ (j : RightMoves x), 0 ⧏ moveRight x j) ↔
    ∀ (j : RightMoves x), 0 ⧏ moveRight x j
simp