no goals
α : Type u_1
β : Type ?u.1175
inst✝¹ : Preorder α
inst✝ : OrderBot α
a✝ b✝ x a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b
simp only [Ne.def, @not_imp_comm (b = ⊥), not_imp, lt_iff_le_not_le]