The order of WithBotTop

Candidates for Mathlib.Order.WithBotTop: an element of the type lies strictly between ⊥ and ⊤ (WithBotTop.bot_lt_coe, WithBotTop.coe_lt_top).

@[simp]

theorem WithBotTop.bot_lt_coe {ι : Type u_1} [LT ι] (a : ι) : ⊥ < coe a

@[simp]

theorem WithBotTop.coe_lt_top {ι : Type u_1} [LT ι] (a : ι) : coe a < ⊤