cases m using binaryRec with
| z => simp
| f b _ _ =>
  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]
n m : ℕ
⊢ Bool.xor (decide (n % 2 = 0)) (decide (m % 2 = 1)) = decide ((n + m) % 2 = 0)
no goals