English
The left-move of a game constructed via ofStateAux is relabelled to a new state constructed by ofStateAux with n−1.
Русский
Левый ход игры, построенной через ofStateAux, переименовывается в новую игру, построенную через ofStateAux с n−1.
LaTeX
$$$\text{relabellingMoveLeftAux}(n,s,h,t) : \text{Relabelling}(\text{moveLeft}(\text{ofStateAux}(n,s,h),t))\; (\text{ofStateAux}(n-1,\, (\text{leftMovesOfStateAux}(n,h) t).2, \text{turnBound_of_left}((\text{leftMovesOfStateAux}(n,h) t).2, n-1, \text{...}))$$$
Lean4
/-- The relabelling showing `moveLeft` applied to a game constructed using `ofStateAux`
has itself been constructed using `ofStateAux`.
-/
def relabellingMoveLeftAux (n : ℕ) {s : S} (h : turnBound s ≤ n) (t : LeftMoves (ofStateAux n s h)) :
Relabelling (moveLeft (ofStateAux n s h) t)
(ofStateAux (n - 1) ((leftMovesOfStateAux n h) t : S)
(turnBound_of_left ((leftMovesOfStateAux n h) t).2 (n - 1) (Nat.le_trans h le_tsub_add))) :=
by
induction n
· have t' := (leftMovesOfStateAux 0 h) t
exfalso; exact turnBound_ne_zero_of_left_move t'.2 (nonpos_iff_eq_zero.mp h)
· rfl
