cases hba with
  | intro z hz =>
    rw [hz] at hw
    have hw1 : b + z + w = b := Eq.symm hw
    rw [add_assoc] at hw1
    have hzw : z + w = 0 := eq_zero_of_add_right_eq_self hw1
    have hzz : z = 0 := add_right_eq_zero hzw
    rw [hzz] at hz
    assumption
case intro
a b : Nat
hba : b ≤ a
w : Nat
hw : b = a + w
⊢ a = b
no goals