∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : (a : α) → Decidable (Order.pred a = a)]
  {a b : WithBot α},
  a < b →
    a ≤
      match b with
      | none => ⊥
      | some a => if Order.pred a = a then ⊥ else ↑(Order.pred a)