# Zulip Chat Archive

## Stream: maths

### Topic: how to prove of find simple theorem

#### Truong Nguyen (Aug 10 2018 at 17:54):

Hi everyone, I am a new user, my question is maybe too simple. Please make it lear for me.

Can you tell me how to find in the library or prove the simple theorem like:

theorem ttt1 (n m: ℕ ) : n <= m → n < m ∨ n = m :=

sorry

#### Mario Carneiro (Aug 10 2018 at 17:56):

the naming convention would call that `lt_or_eq_of_le`

#### Truong Nguyen (Aug 10 2018 at 22:04):

Thank you, but can you tell me how can find the stuffs like this one?

Is there a “search” command to find a theorem in the library?

I am working in some proof, sometime, it looks me quite a lot of time to find simple theorem to use.

For example, I need this one:

theorem tq (a b: ℕ ): ¬ a ≤ b ↔ b < a :=

sorry

Is there a way that I can find or prove it easily? I think it should be easy.

Thank you,

Truong

#### Kenny Lau (Aug 10 2018 at 22:10):

import tactic.find tactic.ring run_cmd tactic.skip #find ¬ _ ≤ _ ↔ _ < _ -- not_le: ∀ {α : Type u} [_inst_1 : linear_order α] {a b : α}, ¬a ≤ b ↔ b < a

#### Kevin Buzzard (Aug 10 2018 at 22:14):

@Truong Nguyen Mario already explained how to find stuff like this -- learn the naming convention :-) Follow the link!

#### Truong Nguyen (Aug 11 2018 at 02:07):

Oh, thank you

#### Truong Nguyen (Aug 31 2018 at 19:20):

Dear Kenny Lau,

Can you give some instruction for how to use the "#find" command?

#### Kevin Buzzard (Aug 31 2018 at 20:35):

import tactic.find def x := 0 -- or anything -- for some reason you can't use #find immediately #find _ + _ ≤ _ + _

Last updated: May 10 2021 at 07:15 UTC