Theorem: IMOSL.IMO2009C1.GameState.isReachable_central_card_add_numMoves_mod_two (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : (Y.centralCards.card + Y.numMoves) % 2 = (c✝.centralCards.card + c✝.numMoves) % 2
⊢ (c✝.centralCards.card + c✝.numMoves) % 2 = (a✝.centralCards.card + a✝.numMoves) % 2
Tactic:
rw [ValidMove_numMoves h0, Nat.add_mod, ValidMove_central_card_mod_two h0,
  ← Nat.add_mod, add_add_add_comm, Nat.add_mod_right]
State after:
no goals