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