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