## Stream: Is there code for X?

### Topic: cardinal.pos_of_one_le

#### Adam Topaz (Jan 22 2021 at 16:32):

I'm having a hard time finding something that proves the following simple thing:

import set_theory.cardinal

example (x : cardinal) (h : 1 ≤ x) : 0 < x := sorry


#### Eric Wieser (Jan 22 2021 at 16:33):

What import do I need for docs#cardinal?

#### Eric Wieser (Jan 22 2021 at 16:33):

Ah, set_theory.cardinal

#### Adam Topaz (Jan 22 2021 at 16:35):

Oh yeah, sorry :)

#### Eric Wieser (Jan 22 2021 at 16:39):

cardinal.zero_lt_one.trans_le h

#### Adam Topaz (Jan 22 2021 at 16:41):

Oh sorry, I had the wrong way around :) I really need

import set_theory.cardinal

example (x : cardinal) (h : 0 < x) : 1 ≤ x := sorry


#### Adam Topaz (Jan 22 2021 at 16:41):

Which seems a bit harder since you need to know there is nothing between $0$ and $1$.

#### Eric Wieser (Jan 22 2021 at 16:48):

docs#cardinal.one_le_iff_pos

#### Eric Wieser (Jan 22 2021 at 16:48):

Or by library_search ;)

#### Adam Topaz (Jan 22 2021 at 16:49):

Library search didn't find it for me... strange :)

Last updated: May 17 2021 at 15:13 UTC