Simple orders

[UPSTREAM] In a simple order the only strict pair is ⊥ < ⊤: mathlib proves each half (IsSimpleOrder.eq_bot_of_lt, IsSimpleOrder.eq_top_of_lt) and the special case Bool.lt_iff, and the characterization holds for every simple order, so a two-element scale inherits it from its IsSimpleOrder instance.

theorem IsSimpleOrder.lt_iff_eq_bot_and_eq_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] {a b : α} : a < b ↔ a = ⊥ ∧ b = ⊤