theorem nonempty_nhds_inter_Ioi {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [TopologicalSpace α] [OrderTopology α] {x : α} {u : Set α} (hu : u ∈ nhds x) (hx : ¬IsMax x) : (u ∩ Set.Ioi x).Nonempty