cases hab with
| intro w hw =>
  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
a b : Nat
hab : a ≤ b
hba : b ≤ a
⊢ a = b
no goals