# Zulip Chat Archive

## Stream: new members

### Topic: Newbie question

#### Jakob Scholbach (Jan 26 2021 at 20:12):

I am really new to lean, and working through §2 here https://leanprover-community.github.io/mathematics_in_lean/basics.html

I am stuck with this one:

```
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
sorry
```

Of course I would like to say: starting from hypothesis h, add -a on the left and use this lemma sub_self mentioned above in the chapter. What is the syntax to achieve this? Thanks!

#### Johan Commelin (Jan 26 2021 at 20:13):

Hey @Jakob Scholbach nice to see you here!

#### Johan Commelin (Jan 26 2021 at 20:13):

Small tip: you can use #backticks to format your code on Zulip

#### Johan Commelin (Jan 26 2021 at 20:16):

You can go two ways. You can work on the hypothesis `h`

. Or you can work "backward" on the goal.

There is a lemma `add_left_cancel`

that could help with backwards reasoning.

#### Johan Commelin (Jan 26 2021 at 20:18):

For a forward step, you could do something like

```
example {R : Type} [comm_ring R] {a b : R} (h : a + b = 0) : -a = b :=
begin
have h2 : -a + (a + b) = -a + 0,
{ rw h },
end
```

#### Johan Commelin (Jan 26 2021 at 20:18):

There are ways of doing this in 1 step. But that's maybe not very enlightening right now.

#### Jakob Scholbach (Jan 26 2021 at 20:21):

Ok, thanks!

#### Alex J. Best (Jan 26 2021 at 20:21):

For working backwards from the goal, you can do something like,

```
import algebra.ring
namespace my_ring
variables {R : Type*} [ring R]
-- BEGIN
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
begin
rw ← add_zero (-a),
rw ← h,
rw neg_add_cancel_left,
end
end my_ring
```

#### Patrick Massot (Jan 26 2021 at 20:26):

Beware the exercise asks to do it only with the lemmas discussed before. So we need to know the list of allowed lemmas (that I don't remember).

#### Alex J. Best (Jan 26 2021 at 20:39):

good point, I updated what I wrote to only use lemmas in the tutorial, it got way shorter too :grinning:

Last updated: May 07 2021 at 00:30 UTC