calc k2 - k + (k2 - k) = k2 + k2 - k - k := by ring
  _ = k + k + b - k -k := by rw[H2]
  _ = b := by ring
case h.a
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = b
no goals