cases n using binaryRec with
| z => cases b <;> simp [← Nat.two_mul]
| f c _ _ =>
  cases b <;> cases c <;> simp [← Nat.two_mul, Nat.mul_add_mod, ← Nat.add_assoc]
case f
n : ℕ
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
⊢ Bool.xor (decide (n % 2 = 0)) (decide (bit b n✝ % 2 = 1)) = decide ((n + bit b n✝) % 2 = 0)
no goals