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

State before:
k : ℕ
⊢ S (4 * k + 2) = S (4 * k)
Tactic:
rw [S_succ, S_succ, add_assoc, add_right_eq_self, x_mul4_add1]
State after:
k : ℕ
⊢ ((bif x (4 * k) then -1 else 1) + bif !x (4 * k) then -1 else 1) = 0

State before:
k : ℕ
⊢ ((bif x (4 * k) then -1 else 1) + bif !x (4 * k) then -1 else 1) = 0
Tactic:
exact (x (4 * k)).recOn rfl rfl
State after:
no goals