cardinal.pos_of_one_le

Stream: Is there code for X?

[Adam Topaz]

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]

What import do I need for docs#cardinal?

[Eric Wieser]

Ah, set_theory.cardinal

[Adam Topaz]

Oh yeah, sorry :)

[Eric Wieser]

cardinal.zero_lt_one.trans_le h

[Adam Topaz]

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]

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

[Eric Wieser]

docs#cardinal.one_le_iff_pos

[Eric Wieser]

Or by library_search ;)

[Adam Topaz]

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