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

State before:
k : ℕ
⊢ x (4 * k + 1) = !x (4 * k)
Tactic:
change x (2 * 2 * k + 1) = !x (2 * 2 * k)
State after:
k : ℕ
⊢ x (2 * 2 * k + 1) = !x (2 * 2 * k)

State before:
k : ℕ
⊢ x (2 * 2 * k + 1) = !x (2 * 2 * k)
Tactic:
rw [mul_assoc, x_mul2, x_mul2_add1,
  ← Nat.bit0_val, Nat.bodd_bit0, Bool.false_xor]
State after:
no goals