case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg i) = -moveLeft (mk α✝ β✝ a✝¹ a✝) i
x : PGame
i : LeftMoves x
⊢ moveRight (-x) (↑toRightMovesNeg i) = -moveLeft x i
cases x
no goals
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg i) = -moveLeft (mk α✝ β✝ a✝¹ a✝) i
rfl