∀ {S : Type u_1} [inst : SetTheory.PGame.State S] (n : ℕ) (x : S) (h : SetTheory.PGame.State.turnBound x ≤ n + 1)
  (i : (SetTheory.PGame.ofStateAux (n + 1) x h).LeftMoves),
  SetTheory.PGame.State.turnBound ↑((SetTheory.PGame.leftMovesOfStateAux (n + 1) h) i) ≤ n + 1 - 1