# Zulip Chat Archive

## Stream: new members

### Topic: not 0 = 2

#### Bolton Bailey (Jan 13 2021 at 13:21):

Very embarrased to ask this, but I've searched the documentation for an hour and cannot find an answer to this very simple question. How does one prove a fact such as `\not 0 = 2`

for naturals?

#### Mario Carneiro (Jan 13 2021 at 13:21):

`dec_trivial`

will work for naturals, `by norm_num`

works in general

#### Mario Carneiro (Jan 13 2021 at 13:22):

Or `two_ne_zero'`

if you just want the exact theorem

#### Bolton Bailey (Jan 13 2021 at 13:26):

Great thanks. How come library_search does not seem to work for this?

#### Damiano Testa (Jan 13 2021 at 13:28):

It may have to do with the fact that the lemma is `2 \neq 0`

. This works:

```
example : 2 ≠ 0 := by library_search
```

as does

```
example : 0 ≠ 2 := by library_search
```

#### Kevin Buzzard (Jan 13 2021 at 13:43):

Why would a *library* have a proof of `\not 0 = 2`

? Do you want it to have a proof that 2 is not 37? It's a finite library. This is the sort of thing you should prove with a *calculation* right?

#### Mario Carneiro (Jan 13 2021 at 13:51):

well, two is an important number

#### Kevin Buzzard (Jan 13 2021 at 13:55):

One has to stop somewhere though. Is three an important number?

My point is really that it's important to learn early on what one expects in a *library* and what one is expected to deal with using results in a library and tactics.

#### Damiano Testa (Jan 13 2021 at 13:56):

Just for fun. This also works:

```
example : 37 ≠ 0 := by library_search
```

#### Damiano Testa (Jan 13 2021 at 13:56):

This *does* look like the library of Babel...

#### Damiano Testa (Jan 13 2021 at 13:58):

I think that we can prove by induction that `library_search`

contains the proof of all lemmas `n.succ \neq 0`

.

#### Kevin Buzzard (Jan 13 2021 at 14:05):

Damiano Testa said:

Just for fun. This also works:

`example : 37 ≠ 0 := by library_search`

Oh yeah, I put that one in because I deemed it important. Wait -- what? What does `by show_term {library_search}`

say?

#### Kevin Buzzard (Jan 13 2021 at 14:05):

Oh -- is it using `succ_ne_zero`

?

#### Damiano Testa (Jan 13 2021 at 14:13):

Yes, this is what it says:

```
Try this: exact 36.succ_ne_zero
```

#### Damiano Testa (Jan 13 2021 at 14:16):

I guess that this means that the library is finite in the sense that you can only check out a finite number of lemmas from it, but the number of lemmas that it contains is not finite...

#### Kevin Buzzard (Jan 13 2021 at 14:18):

this is a lemma with a variable input so really it's a family of lemmas

#### Damiano Testa (Jan 13 2021 at 14:21):

Maybe we should define flat families of lemmas...

#### Kevin Buzzard (Jan 13 2021 at 15:06):

I think they might all be flat

Last updated: May 08 2021 at 03:17 UTC