cases m 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
m : ℕ
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (m % 2 = 0)) = decide ((bit b n✝ + m) % 2 = 1)
⊢ Bool.xor (decide (bit b n✝ % 2 = 0)) (decide (m % 2 = 0)) = decide ((bit b n✝ + m) % 2 = 1)
no goals