Principal upper sets at two points

The principal upper sets UpperSet.Ici a and UpperSet.Ioi a compared across points: the upper set strictly above a point is weaker than the one from any greater point, and the upper set from a point is covered by the one strictly above it, the two differing only in the point itself. The lemmas restate Set.Ici_subset_Ioi and the cover of Set.Ioi a by Set.Ici a for upper sets, and are [UPSTREAM] additions to Mathlib.Order.UpperLower.Principal.

theorem UpperSet.Ioi_le_Ici {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : Ioi a ≤ Ici b

theorem UpperSet.Ici_covBy_Ioi {α : Type u_1} [PartialOrder α] (a : α) : Ici a ⋖ Ioi a