∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β}, b < f (List.minOn f xs h) ↔ ∀ x ∈ xs, b < f x