## 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: Dec 20 2023 at 11:08 UTC