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

State before:
n : ℕ
X Y : GameState n
h : X.ValidMove Y
i : ℕ
x✝ : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.centralCards.card % 2 =
    (X.centralCards.card + 1) % 2
Tactic:
rw [centralCards, filter_symmDiff, ← centralCards,
  symmDiff_card_mod_two, Iic_filter_dvd_card]
State after:
no goals