# Zulip Chat Archive

## Stream: new members

### Topic: add_right_cancel natural number game

#### Thomas Laraia (Jul 04 2021 at 08:36):

Hi, I am working on add_right_cancel in Advanced Addition World and am not understanding why I cannot apply succ_inj to the h hypothesis. I can see the steps that need to be taken but maybe I need to take a more roundabout way?

```
intro h,
induction t with d hd,
rw add_zero at h,
rw add_zero at h,
rw h,
refl,
repeat {rw add_succ at h},
apply succ_inj at h,
```

#### Thomas Laraia (Jul 04 2021 at 08:42):

And at the same time, if I just `apply succ_inj`

, the goal changes from `a = b`

to `succ a = succ b`

, which feels like the opposite of what `succ_inj`

is supposed to do.

#### Ruben Van de Velde (Jul 04 2021 at 08:58):

You've fallen victim to a common misunderstanding about `apply`

. `apply`

means "I've got a lemma whose conclusion matches the goal, so to prove my goal, it suffices to prove the hypothesis of this lemma"

#### Ruben Van de Velde (Jul 04 2021 at 09:01):

In this case, you want to use `succ_inj {a b : mynat} : succ(a) = succ(b) → a = b`

with the hypothesis `h : succ (a + d) = succ (b + d)`

to conclude `a + d = b + d`

; you do that by treating → as a function application: `have h2 := succ_inj h,`

#### Ruben Van de Velde (Jul 04 2021 at 09:03):

Alternatively, you can go backwards from the goal and claim it suffices to prove `a + d = b + d`

by `apply hd,`

#### Thomas Laraia (Jul 04 2021 at 09:08):

Perfect, thank you for the explanation!

Last updated: Dec 20 2023 at 11:08 UTC