# Zulip Chat Archive

## Stream: general

### Topic: n + 1 = 1 -> n = 0

#### Valéry Croizier (Jun 28 2020 at 15:17):

Hi, Lean and Zulip newbie there, not sure where to post exactly. Stuck on this calculation. How to prove it?

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:19):

Welcome! Is this what you want:

```
example (n : ℕ) : n+1 = 1 → n = 0 := nat.succ.inj
```

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:20):

In general you can find lemmas from the library with `library_search`

:

```
import tactic
example (n : ℕ) : n+1 = 1 → n = 0 := by library_search
```

#### Valéry Croizier (Jun 28 2020 at 15:22):

Is this a reference to succ_inj in nat/lemmas ?

#### Johan Commelin (Jun 28 2020 at 15:22):

@Valéry Croizier To explain why `nat.succ.inj`

proves this: `n + 1 = succ n`

by definition, and `1 = succ 0`

, by definition.

#### Valéry Croizier (Jun 28 2020 at 15:23):

My Lean doesn't know library_search :(

#### Johan Commelin (Jun 28 2020 at 15:23):

Did you `import tactic`

?

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:23):

I think `nat.succ_inj`

was renamed to `nat.succ.inj`

recently, so it may depend on what version of Lean you're using.

#### Valéry Croizier (Jun 28 2020 at 15:23):

I use VSCode and elan on WSL2.

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:24):

See #install for instructions on installing the latest version of Lean along with mathlib.

#### Valéry Croizier (Jun 28 2020 at 15:25):

My install is just a few days old. leanpkg.toml says leanprover-community/lean:3.16.4.

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:26):

Then `example (n : ℕ) : n+1 = 1 → n = 0 := nat.succ.inj`

should work...

#### Valéry Croizier (Jun 28 2020 at 15:26):

Anyway, nat.succ.inj works, so thank you very much for you help.

#### Bryan Gin-ge Chen (Jun 28 2020 at 15:27):

I recommend figuring out how to install mathlib so you can use `library_search`

and other tactic goodies though. Let us know if you have any trouble.

#### Valéry Croizier (Jun 28 2020 at 15:35):

OK, library_search missed some imports mentioned in the doc. Nice. :slight_smile:

Last updated: Dec 20 2023 at 11:08 UTC