Swiching both sides of the equation

Stream: lean4

[Denson Cash]

I am currently working through "Mathematics in Lean" and reached chapter 2, section 2. There, I already proved eq_neg_of_add_eq_zero the following way:

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  rw [← add_left_neg b] at h
  exact add_right_cancel h

Now I want to prove neg_eq_of_add_eq_zero similiarly, but this doesn't work:

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  rw [← add_right_neg a] at h
  exact add_left_cancel h

application type mismatch
  add_left_cancel h
argument
  h
has type
  a + b = a + -a : Prop
but is expected to have type
  a + -a = a + b : Prop

I guess Lean needs me to switch both sides of the equation in h before finishing with exact add_left_cancel hand I was wondering how to that. Also, feel free to suggest improvements of my code.

[Pedro Sánchez Terraf]

h.symm is hwith sides switched.

[Patrick Massot]

The intended solution uses neg_add_cancel_left.

[Patrick Massot]

But of course there are many ways to prove this.

[Denson Cash]

My current working solution looks like this (thanks to Pedro Sánchez Terraf):

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  rw [← add_right_neg a] at h
  exact add_left_cancel h.symm