Theorem: IMOSL.IMO2010A4.S_parity (IMOSLLean4/IMO2010/A4/A4.lean)

State before:
k : ℕ
h : (S k).bodd = k.bodd
⊢ (S k.succ).bodd = k.succ.bodd
Tactic:
rw [Nat.bodd_succ, S_succ, Int.bodd_add, h, ← Bool.xor_true]
State after:
k : ℕ
h : (S k).bodd = k.bodd
⊢ xor k.bodd (bif x k then -1 else 1).bodd = xor k.bodd true

State before:
k : ℕ
h : (S k).bodd = k.bodd
⊢ xor k.bodd (bif x k then -1 else 1).bodd = xor k.bodd true
Tactic:
exact (x k).rec rfl rfl
State after:
no goals